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 📖	mathematical	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	Function.Bijective DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLike	—	surjective_of_surjective_of_injective_of_left_exact
bijective_of_surjective_of_bijective_of_bijective_of_injective 📖	mathematical	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	Function.Bijective DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLike	—	injective_of_surjective_of_injective_of_injective surjective_of_surjective_of_surjective_of_injective
bijective_of_surjective_of_bijective_of_right_exact 📖	mathematical	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	Function.Bijective DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLike	—	injective_of_surjective_of_injective_of_right_exact
injective_of_surjective_of_injective_of_injective 📖	mathematical	comp AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Function.Exact DFunLike.coe AddMonoidHom instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLike	—	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 📖	mathematical	comp AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Function.Exact DFunLike.coe AddMonoidHom instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLike	—	injective_of_surjective_of_injective_of_injective comp_zero Set.mem_range
surjective_of_surjective_of_injective_of_left_exact 📖	mathematical	comp AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Function.Exact DFunLike.coe AddMonoidHom instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLike	—	surjective_of_surjective_of_surjective_of_injective comp_zero Set.mem_range map_zero AddMonoidHomClass.toZeroHomClass instAddMonoidHomClass
surjective_of_surjective_of_surjective_of_injective 📖	mathematical	comp AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Function.Exact DFunLike.coe AddMonoidHom instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instFunLike	—	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 📖	mathematical	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	Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	—	RingHomCompTriple.ids surjective_of_surjective_of_injective_of_left_exact
bijective_of_surjective_of_bijective_of_bijective_of_injective 📖	mathematical	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	Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	—	RingHomCompTriple.ids injective_of_surjective_of_injective_of_injective surjective_of_surjective_of_surjective_of_injective
bijective_of_surjective_of_bijective_of_right_exact 📖	mathematical	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	Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	—	RingHomCompTriple.ids injective_of_surjective_of_injective_of_right_exact
injective_of_surjective_of_injective_of_injective 📖	mathematical	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	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	—	RingHomCompTriple.ids AddMonoidHom.injective_of_surjective_of_injective_of_injective AddMonoidHom.ext DFunLike.congr_fun
injective_of_surjective_of_injective_of_right_exact 📖	mathematical	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	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	—	RingHomCompTriple.ids injective_of_surjective_of_injective_of_injective comp_zero
surjective_of_surjective_of_injective_of_left_exact 📖	mathematical	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	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	—	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 📖	mathematical	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	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	—	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 📖	mathematical	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	Function.Bijective DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLike	—	surjective_of_surjective_of_injective_of_left_exact
bijective_of_surjective_of_bijective_of_bijective_of_injective 📖	mathematical	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	Function.Bijective DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLike	—	injective_of_surjective_of_injective_of_injective surjective_of_surjective_of_surjective_of_injective
bijective_of_surjective_of_bijective_of_right_exact 📖	mathematical	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	Function.Bijective DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLike	—	injective_of_surjective_of_injective_of_right_exact
injective_of_surjective_of_injective_of_injective 📖	mathematical	comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Function.MulExact DFunLike.coe MonoidHom instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLike	—	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 📖	mathematical	comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Function.MulExact DFunLike.coe MonoidHom instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLike	—	injective_of_surjective_of_injective_of_injective comp_one
surjective_of_surjective_of_injective_of_left_exact 📖	mathematical	comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Function.MulExact DFunLike.coe MonoidHom instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLike	—	surjective_of_surjective_of_surjective_of_injective comp_one map_one MonoidHomClass.toOneHomClass instMonoidHomClass
surjective_of_surjective_of_surjective_of_injective 📖	mathematical	comp MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Function.MulExact DFunLike.coe MonoidHom instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instFunLike	—	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