LeftExact

Statistics

Metric	Count
Definitions	0
Theorems `exact_lcomp_of_exact_of_surjective`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`exact_lcomp_of_exact_of_surjective` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `lcomp` `instZero`	—	`smulCommClass_self` `RingHomCompTriple.ids` `RingHomSurjective.ids` `range_le_ker_iff` `RingHomInvPair.ids` `ext` `Function.Exact.linearEquivOfSurjective_symm_apply` `comp_assoc` `Function.Exact.linearMap_comp_eq_zero` `comp_zero`

---