Documentation Verification Report

Units

📁 Source: Mathlib/Algebra/GroupWithZero/Action/Units.lean

Statistics

Metric	Count
Definitions `smulRight`, `instDistribMulAction`, `instDistribSMulUnits`, `instMulDistribMulAction`, `instSMulZeroClass`	5
Theorems `smul_left_iff₀`, `smul_right_iff₀`, `smulRight_apply`, `smulRight_symm_apply`, `smul_eq_zero`, `smul_mk0`, `eq_inv_smul_iff₀`, `inv_smul_eq_iff₀`, `inv_smul_smul₀`, `smul_inv_smul₀`	10
Total	15

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_left_iff₀` 📖	mathematical	—	`Commute` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`smul_left_iff` `Units.smulCommClass_left` `Units.instIsScalarTower`
`smul_right_iff₀` 📖	mathematical	—	`Commute` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`smul_right_iff` `Units.smulCommClass_left` `Units.instIsScalarTower`

Equiv

Definitions

Name	Category	Theorems
`smulRight` 📖	CompOp	2 math math: `smulRight_symm_apply`, `smulRight_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smulRight_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `smulRight` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	—
`smulRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm` `smulRight` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	—

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_eq_zero` 📖	mathematical	`IsUnit`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`smul_eq_zero_iff_eq`

Units

Definitions

Name	Category	Theorems
`instDistribMulAction` 📖	CompOp	24 math math: `units_inv_smul`, `Module.Ray.neg_units_smul`, `Module.Ray.units_smul_of_neg`, `Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe`, `units_smul_eq_self_iff`, `units_smul_eq_neg_iff`, `Module.Ray.units_smul_of_pos`, `Orientation.map_eq_det_inv_smul`, `SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply`, `SpecialLinearGroup.centerEquivRootsOfUnity_apply`, `Module.Basis.map_orientation_eq_det_inv_smul`, `LinearEquiv.smulOfNeZero_symm_apply`, `IsCyclic.mulAutMulEquiv_symm_apply_symm_apply`, `AddAut.mulLeft_apply_apply`, `TensorProduct.CompatibleSMul.unit`, `Module.Basis.orientation_unitsSMul`, `IsCyclic.mulAutMulEquiv_symm_apply_apply`, `autEquivRootsOfUnity_apply_rootOfSplit`, `SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply`, `Projectivization.generalLinearGroup_smul_def`, `AddAut.mulLeft_apply_symm_apply`, `LinearEquiv.smul_refl`, `QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate'`, `autEquivRootsOfUnity_smul`
`instDistribSMulUnits` 📖	CompOp	—
`instMulDistribMulAction` 📖	CompOp	—
`instSMulZeroClass` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_mk0` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `instSMul`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_inv_smul_iff₀` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`eq_inv_smul_iff`
`inv_smul_eq_iff₀` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`inv_smul_eq_iff`
`inv_smul_smul₀` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`inv_smul_smul`
`smul_inv_smul₀` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`smul_inv_smul`

---

← Back to Index