Documentation Verification Report

FreeRing

📁 Source: Mathlib/RingTheory/FreeRing.lean

Statistics

Metric	Count
Definitions `FreeRing`, `map`, `of`, `instInhabitedFreeRing`, `instRingFreeRing`	5
Theorems `hom_ext`, `hom_ext_iff`, `induction_on`, `lift_comp_of`, `lift_of`, `map_of`, `of_injective`, `of_ne_one`, `of_ne_zero`, `one_ne_of`, `zero_ne_of`, `instNontrivialFreeRing`	12
Total	17

FreeRing

Definitions

Name	Category	Theorems
`map` 📖	CompOp	1 math math: `map_of`
`of` 📖	CompOp	6 math math: `of_injective`, `map_of`, `coe_of`, `hom_ext_iff`, `lift_comp_of`, `lift_of`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_ext` 📖	—	`DFunLike.coe` `RingHom` `FreeRing` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingFreeRing` `RingHom.instFunLike` `of`	—	—	`Equiv.injective`
`hom_ext_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeRing` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingFreeRing` `RingHom.instFunLike` `of`	—	`hom_ext`
`induction_on` 📖	—	`FreeRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `instRingFreeRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `of` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul`	—	—	`neg_one_mul` `neg_neg` `FreeAbelianGroup.induction_on` `neg_add_cancel`
`lift_comp_of` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RingHom` `FreeRing` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingFreeRing` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `RingHom.instFunLike` `of`	—	`Equiv.right_inv`
`lift_of` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeRing` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingFreeRing` `RingHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `of`	—	`Equiv.left_inv`
`map_of` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeRing` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingFreeRing` `RingHom.instFunLike` `map` `of`	—	`lift_of`
`of_injective` 📖	mathematical	—	`FreeRing` `of`	—	`FreeAbelianGroup.of_injective` `FreeMonoid.of_injective`
`of_ne_one` 📖	—	—	—	—	`FreeAbelianGroup.of_injective` `FreeMonoid.of_ne_one`
`of_ne_zero` 📖	—	—	—	—	`FreeAbelianGroup.of_ne_zero`
`one_ne_of` 📖	—	—	—	—	`FreeAbelianGroup.of_injective` `FreeMonoid.one_ne_of`
`zero_ne_of` 📖	—	—	—	—	`FreeAbelianGroup.zero_ne_of`

(root)

Definitions

Name	Category	Theorems
`FreeRing` 📖	CompOp	16 math math: `instNontrivialFreeRing`, `FreeRing.of_injective`, `FreeRing.coe_one`, `FreeRing.coe_neg`, `FreeRing.coe_zero`, `FreeRing.map_of`, `FreeRing.coe_add`, `FreeRing.hom_ext_iff`, `Cardinal.mk_freeRing`, `FreeRing.lift_comp_of`, `FreeRing.lift_of`, `FreeRing.coe_surjective`, `FreeRing.coe_sub`, `instInfiniteFreeRing`, `FreeRing.coe_mul`, `instCountableFreeRing`
`instInhabitedFreeRing` 📖	CompOp	—
`instRingFreeRing` 📖	CompOp	10 math math: `FreeRing.coe_one`, `FreeRing.coe_neg`, `FreeRing.coe_zero`, `FreeRing.map_of`, `FreeRing.coe_add`, `FreeRing.hom_ext_iff`, `FreeRing.lift_comp_of`, `FreeRing.lift_of`, `FreeRing.coe_sub`, `FreeRing.coe_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNontrivialFreeRing` 📖	mathematical	—	`Nontrivial` `FreeRing`	—	`FreeAbelianGroup.instNontrivialOfNonempty`

---

← Back to Index