Documentation Verification Report

Lemmas

📁 Source: Mathlib/Algebra/Group/Irreducible/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems `addIrreducible_iff`, `map`, `not_even`, `not_addIrreducible`, `map`, `not_isSquare`, `of_map`, `not_irreducible`, `irreducible_iff`, `addIrreducible_addUnits_add`, `addIrreducible_add_addUnits`, `addIrreducible_add_iff`, `addIrreducible_add_isAddUnit`, `addIrreducible_isAddUnit_add`, `irreducible_isUnit_mul`, `irreducible_mul_iff`, `irreducible_mul_isUnit`, `irreducible_mul_units`, `irreducible_units_mul`, `not_addIrreducible_nsmul`, `not_irreducible_pow`	21
Total	21

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addIrreducible_iff` 📖	mathematical	—	`AddIrreducible` `DFunLike.coe` `EquivLike.toFunLike`	—	`addIrreducible_iff` `isAddUnit_map` `Function.Surjective.forall` `EquivLike.surjective` `map_add` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `EmbeddingLike.apply_eq_iff_eq` `EquivLike.toEmbeddingLike`

AddIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`AddIrreducible`	`DFunLike.coe` `EquivLike.toFunLike`	—	`AddEquiv.addIrreducible_iff`
`not_even` 📖	mathematical	`AddIrreducible`	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`even_iff_exists_two_nsmul` `not_addIrreducible_nsmul`

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_addIrreducible` 📖	mathematical	`Even` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddIrreducible`	—	`AddIrreducible.not_even`

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`Irreducible`	`DFunLike.coe` `EquivLike.toFunLike`	—	`MulEquiv.irreducible_iff`
`not_isSquare` 📖	mathematical	`Irreducible`	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`isSquare_iff_exists_sq` `not_irreducible_pow`
`of_map` 📖	—	`Irreducible` `DFunLike.coe`	—	—	`not_isUnit` `IsUnit.map` `IsUnit.of_map` `isUnit_or_isUnit` `map_mul` `MonoidHomClass.toMulHomClass`

IsSquare

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_irreducible` 📖	mathematical	`IsSquare` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Irreducible`	—	`Irreducible.not_isSquare`

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_iff` 📖	mathematical	—	`Irreducible` `DFunLike.coe` `EquivLike.toFunLike`	—	`Function.Surjective.forall` `EquivLike.surjective` `MonoidHomClass.toMulHomClass` `MulEquivClass.instMonoidHomClass` `EquivLike.toEmbeddingLike`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addIrreducible_addUnits_add` 📖	mathematical	—	`AddIrreducible` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.val`	—	`addIrreducible_iff` `AddUnits.isAddUnit_addUnits_add` `add_assoc` `AddUnits.neg_add_cancel_left`
`addIrreducible_add_addUnits` 📖	mathematical	—	`AddIrreducible` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.val`	—	`addIrreducible_iff` `AddUnits.isAddUnit_add_addUnits` `add_assoc` `AddUnits.add_neg_cancel_right`
`addIrreducible_add_iff` 📖	mathematical	—	`AddIrreducible` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `IsAddUnit`	—	`addIrreducible_add_isAddUnit` `addIrreducible_isAddUnit_add` `AddIrreducible.isAddUnit_or_isAddUnit`
`addIrreducible_add_isAddUnit` 📖	mathematical	`IsAddUnit`	`AddIrreducible` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`addIrreducible_add_addUnits`
`addIrreducible_isAddUnit_add` 📖	mathematical	`IsAddUnit`	`AddIrreducible` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`addIrreducible_addUnits_add`
`irreducible_isUnit_mul` 📖	mathematical	`IsUnit`	`Irreducible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`irreducible_units_mul`
`irreducible_mul_iff` 📖	mathematical	—	`Irreducible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `IsUnit`	—	`irreducible_mul_isUnit` `irreducible_isUnit_mul` `Irreducible.isUnit_or_isUnit`
`irreducible_mul_isUnit` 📖	mathematical	`IsUnit`	`Irreducible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`irreducible_mul_units`
`irreducible_mul_units` 📖	mathematical	—	`Irreducible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.val`	—	`Units.isUnit_mul_units` `mul_assoc` `Units.mul_inv_cancel_right`
`irreducible_units_mul` 📖	mathematical	—	`Irreducible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.val`	—	`Units.isUnit_units_mul` `mul_assoc` `Units.inv_mul_cancel_left`
`not_addIrreducible_nsmul` 📖	mathematical	—	`AddIrreducible` `AddMonoid.toNatSMul`	—	`zero_nsmul` `not_addIrreducible_zero` `succ_nsmul` `IsAddUnit.nsmul` `isAddUnit_nsmul_iff`
`not_irreducible_pow` 📖	mathematical	—	`Irreducible` `Monoid.toNatPow`	—	`pow_zero` `pow_succ` `IsUnit.pow` `isUnit_pow_iff`

---

← Back to Index