Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `AddIrreducible`	1
Theorems `eq_zero_or_eq_zero`, `isAddUnit_or_isAddUnit`, `ne_zero`, `not_isAddUnit`, `eq_one_or_eq_one`, `isUnit_or_isUnit`, `ne_one`, `not_isUnit`, `addIrreducible_iff`, `addIrreducible_or_factor`, `irreducible_iff`, `irreducible_or_factor`, `not_addIrreducible_zero`, `not_irreducible_one`, `of_addIrreducible_add`, `of_irreducible_mul`	16
Total	17

AddIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_or_eq_zero` 📖	mathematical	`AddIrreducible` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddZero.toZero`	—	`isAddUnit_iff_eq_zero` `isAddUnit_or_isAddUnit`
`isAddUnit_or_isAddUnit` 📖	mathematical	`AddIrreducible` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`IsAddUnit`	—	—
`ne_zero` 📖	—	`AddIrreducible`	—	—	`not_addIrreducible_zero`
`not_isAddUnit` 📖	mathematical	`AddIrreducible`	`IsAddUnit`	—	—

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_one_or_eq_one` 📖	mathematical	`Irreducible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`MulOne.toOne`	—	`isUnit_or_isUnit`
`isUnit_or_isUnit` 📖	mathematical	`Irreducible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsUnit`	—	—
`ne_one` 📖	—	`Irreducible`	—	—	`not_irreducible_one`
`not_isUnit` 📖	mathematical	`Irreducible`	`IsUnit`	—	—

(root)

Definitions

Name	Category	Theorems
`AddIrreducible` 📖	CompData	17 math math: `not_addIrreducible_zero`, `AddSubmonoid.closure_addIrreducible`, `addIrreducible_add_isAddUnit`, `addIrreducible_add_iff`, `addIrreducible_isAddUnit_add`, `addIrreducible_iff`, `isAddIndecomposable_id_univ`, `addIrreducible_subset_of_addSubmonoidClosure_eq_top`, `addIrreducible_or_factor`, `not_addIrreducible_nsmul`, `addIrreducible_mem_addSubmonoidClosure_subset`, `addIrreducible_add_addUnits`, `AddEquiv.addIrreducible_iff`, `finite_addIrreducible`, `Even.not_addIrreducible`, `addIrreducible_addUnits_add`, `AddSubmonoid.FG.finite_addIrreducible_mem_addSubmonoidClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addIrreducible_iff` 📖	mathematical	—	`AddIrreducible` `IsAddUnit`	—	`AddIrreducible.not_isAddUnit` `AddIrreducible.isAddUnit_or_isAddUnit`
`addIrreducible_or_factor` 📖	mathematical	`IsAddUnit`	`AddIrreducible` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`addIrreducible_iff` `em`
`irreducible_iff` 📖	mathematical	—	`Irreducible` `IsUnit`	—	`Irreducible.not_isUnit` `Irreducible.isUnit_or_isUnit`
`irreducible_or_factor` 📖	mathematical	`IsUnit`	`Irreducible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`em`
`not_addIrreducible_zero` 📖	mathematical	—	`AddIrreducible` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`addIrreducible_iff` `isAddUnit_zero`
`not_irreducible_one` 📖	mathematical	—	`Irreducible` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`of_addIrreducible_add` 📖	mathematical	`AddIrreducible` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`IsAddUnit`	—	—
`of_irreducible_mul` 📖	mathematical	`Irreducible` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsUnit`	—	—

---

← Back to Index