Documentation Verification Report

AddAut

📁 Source: Mathlib/Algebra/Ring/AddAut.lean

Statistics

Metric	Count
Definitions `AddAut`, `mulLeft`, `mulRight`	3
Theorems `mulLeft_apply_apply`, `mulLeft_apply_symm_apply`, `mulRight_apply`, `mulRight_symm_apply`	4
Total	7

AddAut

Definitions

Name	Category	Theorems
`mulLeft` 📖	CompOp	3 math math: `ZMod.AddAutEquivUnits_symm_apply`, `mulLeft_apply_apply`, `mulLeft_apply_symm_apply`
`mulRight` 📖	CompOp	2 math math: `mulRight_symm_apply`, `mulRight_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeft_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `MonoidHom` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddAut` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MulOneClass.toMulOne` `Units.instMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MonoidHom.instFunLike` `mulLeft` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Units.instGroup` `Units.instDistribMulAction` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule`	—	—
`mulLeft_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `MonoidHom` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddAut` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MulOneClass.toMulOne` `Units.instMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MonoidHom.instFunLike` `mulLeft` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instGroup` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `Units.instDistribMulAction` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`mulRight_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `mulRight` `Distrib.toMul` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—
`mulRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `mulRight` `Distrib.toMul` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `Units.instInv`	—	—

(root)

Definitions

Name	Category	Theorems
`AddAut` 📖	CompOp	41 math math: `AddAut.inv_symm`, `AddAut.apply_inv_self`, `AddAutAdditive_apply_symm_apply`, `AddAut.mul_apply`, `AddAction.stabilizer_vadd_eq_stabilizer_map_conj`, `Set.conj_mem_fixingAddSubgroup`, `AddAutAdditive_apply_apply`, `AddAutAdditive_symm_apply_symm_apply`, `MulAutMultiplicative_symm_apply_apply`, `ZMod.AddAutEquivUnits_symm_apply`, `MulAutMultiplicative_apply_apply`, `AddAut.conj_symm_apply`, `AddAut.coe_inv`, `MulAutMultiplicative_symm_apply_symm_apply`, `AddAut.coe_mul`, `AddAction.stabilizerEquivStabilizer_symm_apply`, `AddAut.conj_inv_apply`, `ZMod.AddAutEquivUnits_apply`, `SubAddAction.fixingAddSubgroup_vadd_eq_fixingAddSubgroup_map_conj`, `AddAction.IsBlock.of_addSubgroup_of_conjugate`, `AddAut.coe_one`, `AddAut.apply_faithfulSMul`, `AddAut.conj_apply`, `AddAut.inv_apply`, `SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup_coe_apply`, `DistribMulAction.toAddAut_apply`, `AddAut.inv_def`, `AddAction.stabilizerEquivStabilizer_apply`, `AddAut.mulLeft_apply_apply`, `MulAutMultiplicative_apply_symm_apply`, `AddAut.one_def`, `AddAut.one_apply`, `AddAut.mulLeft_apply_symm_apply`, `SubAddAction.fixingAddSubgroup_map_conj_eq`, `AddAut.smul_def`, `AddAut.neg_conj_apply`, `AddAut.mul_def`, `AddAutAdditive_symm_apply_apply`, `AddAut.congr_apply`, `AddAut.inv_apply_self`, `AddAut.congr_symm_apply`

---

← Back to Index