feat(Algebra): IsUnital and IsNotUnital classes

[themathqueen]

This adds Prop-type classes on multiplicative types that state whether a unit exists or not. This shouldn't really be used unless it is the only reasonable way to phrase or prove a statement.

---

This will be used in #36327.

Zulip thread: #mathlib4 > `IsUnital` class

[github-actions]

PR summary 1527acd198

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ IsNotUnital
+ IsUnital
+ IsUnital.toAlgebra
+ IsUnital.toCStarAlgebra
+ IsUnital.toCommCStarAlgebra
+ IsUnital.toMonoid
+ IsUnital.toMulOneClass
+ MulOneClass.isUnital
+ not_isNotUnital_iff_isUnital
+ not_isUnital_iff_isNotUnital
+ toCommRing
+ toCommSemiring
+ toNonAssocCommRing
+ toNonAssocCommSemiring
+ toNonAssocRing
+ toNonAssocSemiring
+ toRing
+ toSemiring

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 1527acd).

• +30 new declarations
• −0 removed declarations

+IsNotUnital
+IsNotUnital.casesOn
+IsNotUnital.isNotUnital
+IsNotUnital.mk
+IsNotUnital.rec
+IsNotUnital.recOn
+IsUnital
+IsUnital.casesOn
+IsUnital.isUnital
+IsUnital.mk
+IsUnital.rec
+IsUnital.recOn
+IsUnital.toAlgebra
+IsUnital.toCStarAlgebra
+IsUnital.toCommCStarAlgebra
+IsUnital.toCommRing
+IsUnital.toCommSemiring
+IsUnital.toMonoid
+IsUnital.toMulOneClass
+IsUnital.toNonAssocCommRing
+IsUnital.toNonAssocCommSemiring
+IsUnital.toNonAssocRing
+IsUnital.toNonAssocSemiring
+IsUnital.toRing
+IsUnital.toSemiring
+MulOneClass.isUnital
+isNotUnital_iff
+isUnital_iff
+not_isNotUnital_iff_isUnital
+not_isUnital_iff_isNotUnital

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.20)

Current number	Change	Type (weak)
5	1	large files

Current commit 1527acd198
Reference commit 8c79cb4f54

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).