Documentation Verification Report

FiveLemma

📁 Source: Mathlib/Algebra/FiveLemma.lean

Statistics

Metric	Count
Definitions	0
Theorems `bijective_of_bijective_of_injective_of_left_exact`, `bijective_of_surjective_of_bijective_of_bijective_of_injective`, `bijective_of_surjective_of_bijective_of_right_exact`, `injective_of_surjective_of_injective_of_injective`, `injective_of_surjective_of_injective_of_right_exact`, `surjective_of_surjective_of_injective_of_left_exact`, `surjective_of_surjective_of_surjective_of_injective`, `bijective_of_bijective_of_injective_of_left_exact`, `bijective_of_surjective_of_bijective_of_bijective_of_injective`, `bijective_of_surjective_of_bijective_of_right_exact`, `injective_of_surjective_of_injective_of_injective`, `injective_of_surjective_of_injective_of_right_exact`, `surjective_of_surjective_of_injective_of_left_exact`, `surjective_of_surjective_of_surjective_of_injective`, `bijective_of_bijective_of_injective_of_left_exact`, `bijective_of_surjective_of_bijective_of_bijective_of_injective`, `bijective_of_surjective_of_bijective_of_right_exact`, `injective_of_surjective_of_injective_of_injective`, `injective_of_surjective_of_injective_of_right_exact`, `surjective_of_surjective_of_injective_of_left_exact`, `surjective_of_surjective_of_surjective_of_injective`	21
Total	21

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_of_bijective_of_injective_of_left_exact` 📖	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Function.Exact` `DFunLike.coe` `AddMonoidHom` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Function.Bijective`	—	—	`surjective_of_surjective_of_injective_of_left_exact`
`bijective_of_surjective_of_bijective_of_bijective_of_injective` 📖	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Function.Exact` `DFunLike.coe` `AddMonoidHom` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Function.Bijective`	—	—	`injective_of_surjective_of_injective_of_injective` `surjective_of_surjective_of_surjective_of_injective`
`bijective_of_surjective_of_bijective_of_right_exact` 📖	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Function.Exact` `DFunLike.coe` `AddMonoidHom` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Function.Bijective`	—	—	`injective_of_surjective_of_injective_of_right_exact`
`injective_of_surjective_of_injective_of_injective` 📖	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Function.Exact` `DFunLike.coe` `AddMonoidHom` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—	`injective_iff_map_eq_zero` `instAddMonoidHomClass` `DFunLike.congr_fun` `map_zero` `AddMonoidHomClass.toZeroHomClass` `map_eq_zero_iff` `Function.Exact.apply_apply_eq_zero`
`injective_of_surjective_of_injective_of_right_exact` 📖	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Function.Exact` `DFunLike.coe` `AddMonoidHom` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—	`injective_of_surjective_of_injective_of_injective` `comp_zero` `Set.mem_range`
`surjective_of_surjective_of_injective_of_left_exact` 📖	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Function.Exact` `DFunLike.coe` `AddMonoidHom` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—	`surjective_of_surjective_of_surjective_of_injective` `comp_zero` `Set.mem_range` `map_zero` `AddMonoidHomClass.toZeroHomClass` `instAddMonoidHomClass`
`surjective_of_surjective_of_surjective_of_injective` 📖	—	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Function.Exact` `DFunLike.coe` `AddMonoidHom` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—	`Function.Exact.apply_apply_eq_zero` `map_eq_zero_iff` `AddMonoidHomClass.toZeroHomClass` `instAddMonoidHomClass` `DFunLike.congr_fun` `map_sub` `sub_self` `map_add` `AddMonoidHomClass.toAddHomClass` `sub_add_cancel`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_of_bijective_of_injective_of_left_exact` 📖	—	`comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Function.Exact` `DFunLike.coe` `LinearMap` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Function.Bijective`	—	—	`RingHomCompTriple.ids` `surjective_of_surjective_of_injective_of_left_exact`
`bijective_of_surjective_of_bijective_of_bijective_of_injective` 📖	—	`comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Function.Exact` `DFunLike.coe` `LinearMap` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Function.Bijective`	—	—	`RingHomCompTriple.ids` `injective_of_surjective_of_injective_of_injective` `surjective_of_surjective_of_surjective_of_injective`
`bijective_of_surjective_of_bijective_of_right_exact` 📖	—	`comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Function.Exact` `DFunLike.coe` `LinearMap` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Function.Bijective`	—	—	`RingHomCompTriple.ids` `injective_of_surjective_of_injective_of_right_exact`
`injective_of_surjective_of_injective_of_injective` 📖	—	`comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Function.Exact` `DFunLike.coe` `LinearMap` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`RingHomCompTriple.ids` `AddMonoidHom.injective_of_surjective_of_injective_of_injective` `AddMonoidHom.ext` `DFunLike.congr_fun`
`injective_of_surjective_of_injective_of_right_exact` 📖	—	`comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Function.Exact` `DFunLike.coe` `LinearMap` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`RingHomCompTriple.ids` `injective_of_surjective_of_injective_of_injective` `comp_zero`
`surjective_of_surjective_of_injective_of_left_exact` 📖	—	`comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Function.Exact` `DFunLike.coe` `LinearMap` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`RingHomCompTriple.ids` `surjective_of_surjective_of_surjective_of_injective` `comp_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass`
`surjective_of_surjective_of_surjective_of_injective` 📖	—	`comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `Function.Exact` `DFunLike.coe` `LinearMap` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`RingHomCompTriple.ids` `AddMonoidHom.surjective_of_surjective_of_surjective_of_injective` `AddMonoidHom.ext` `DFunLike.congr_fun`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_of_bijective_of_injective_of_left_exact` 📖	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Function.MulExact` `DFunLike.coe` `MonoidHom` `instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Function.Bijective`	—	—	`surjective_of_surjective_of_injective_of_left_exact`
`bijective_of_surjective_of_bijective_of_bijective_of_injective` 📖	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Function.MulExact` `DFunLike.coe` `MonoidHom` `instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Function.Bijective`	—	—	`injective_of_surjective_of_injective_of_injective` `surjective_of_surjective_of_surjective_of_injective`
`bijective_of_surjective_of_bijective_of_right_exact` 📖	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Function.MulExact` `DFunLike.coe` `MonoidHom` `instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Function.Bijective`	—	—	`injective_of_surjective_of_injective_of_right_exact`
`injective_of_surjective_of_injective_of_injective` 📖	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Function.MulExact` `DFunLike.coe` `MonoidHom` `instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—	`injective_iff_map_eq_one` `instMonoidHomClass` `DFunLike.congr_fun` `map_one` `MonoidHomClass.toOneHomClass` `map_eq_one_iff` `Function.MulExact.apply_apply_eq_one`
`injective_of_surjective_of_injective_of_right_exact` 📖	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Function.MulExact` `DFunLike.coe` `MonoidHom` `instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—	`injective_of_surjective_of_injective_of_injective` `comp_one`
`surjective_of_surjective_of_injective_of_left_exact` 📖	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Function.MulExact` `DFunLike.coe` `MonoidHom` `instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—	`surjective_of_surjective_of_surjective_of_injective` `comp_one` `map_one` `MonoidHomClass.toOneHomClass` `instMonoidHomClass`
`surjective_of_surjective_of_surjective_of_injective` 📖	—	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Function.MulExact` `DFunLike.coe` `MonoidHom` `instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—	`Function.MulExact.apply_apply_eq_one` `map_eq_one_iff` `MonoidHomClass.toOneHomClass` `instMonoidHomClass` `DFunLike.congr_fun` `map_div` `div_self'` `map_mul` `MonoidHomClass.toMulHomClass` `div_mul_cancel`

---

← Back to Index