Exact

📁 Source: Mathlib/Algebra/Exact.lean

Statistics

Metric	Count
Definitions `linearEquivOfSurjective`, `splitInjectiveEquiv`, `splitSurjectiveEquiv`, `MulExact`	4
Theorems `exact_iff`, `exact_iff_of_surjective_of_bijective_of_injective`, `exact_of_comp_eq_zero_of_ker_le_range`, `exact_of_comp_of_mem_range`, `addMonoidHom_comp_eq_zero`, `addMonoidHom_ker_eq`, `addMonoidHom_rangeRestrict`, `apply_apply_eq_zero`, `comp_eq_zero`, `comp_injective`, `exact_mapQ_iff`, `iff_addMonoidHom_rangeRestrict`, `iff_linearMap_rangeRestrict`, `iff_of_ladder_addEquiv`, `iff_of_ladder_linearEquiv`, `iff_rangeFactorization`, `inl_snd`, `inr_fst`, `linearEquivOfSurjective_apply`, `linearEquivOfSurjective_symm_apply`, `linearMap_comp_eq_zero`, `linearMap_ker_eq`, `linearMap_rangeRestrict`, `of_comp_eq_zero_of_ker_in_range`, `of_comp_of_mem_range`, `of_ladder_addEquiv_of_exact`, `of_ladder_addEquiv_of_exact'`, `of_ladder_linearEquiv_of_exact`, `rangeFactorization`, `split_tfae`, `split_tfae'`, `comp_exact_iff_exact`, `apply_apply_eq_one`, `comp_eq_one`, `comp_injective`, `iff_monoidHom_rangeRestrict`, `iff_of_ladder_mulEquiv`, `iff_rangeFactorization`, `monoidHom_comp_eq_zero`, `monoidHom_ker_eq`, `monoidHom_rangeRestrict`, `of_comp_eq_one_of_ker_in_range`, `of_comp_of_mem_range`, `of_ladder_mulEquiv_of_mulExact`, `of_ladder_mulEquiv_of_mulExact'`, `rangeFactorization`, `comp_exact_iff_exact`, `conj_exact_iff_exact`, `exact_iff`, `exact_iff_of_surjective_of_bijective_of_injective`, `exact_map_mkQ_range`, `exact_of_comp_eq_zero_of_ker_le_range`, `exact_of_comp_of_mem_range`, `exact_subtype_ker_map`, `exact_subtype_mkQ`, `exact_zero_iff_injective`, `exact_zero_iff_surjective`, `injective_range_liftQ_of_exact`, `ker_eq_bot_range_liftQ_iff`, `surjective_range_liftQ`, `mulExact_iff`, `mulExact_iff_of_surjective_of_bijective_of_injective`, `mulExact_of_comp_eq_one_of_ker_le_range`, `mulExact_of_comp_of_mem_range`	64
Total	68

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact_iff` 📖	mathematical	—	`Function.Exact` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `ker` `range`	—	`SetLike.ext_iff`
`exact_iff_of_surjective_of_bijective_of_injective` 📖	mathematical	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `instFunLike` `Function.Bijective`	`Function.Exact` `AddZero.toZero`	—	`DFunLike.congr_fun` `map_zero` `AddMonoidHomClass.toZeroHomClass` `instAddMonoidHomClass` `Function.Exact.apply_apply_eq_zero`
`exact_of_comp_eq_zero_of_ker_le_range` 📖	mathematical	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom` `instZeroAddMonoidHom` `AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `ker` `range`	`Function.Exact` `DFunLike.coe` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Function.Exact.of_comp_of_mem_range`
`exact_of_comp_of_mem_range` 📖	mathematical	`comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom` `instZeroAddMonoidHom` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `range`	`Function.Exact` `DFunLike.coe` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`exact_of_comp_eq_zero_of_ker_le_range`

Function

Definitions

Name	Category	Theorems
`MulExact` 📖	MathDef	11 math math: `MulExact.iff_rangeFactorization`, `MulExact.of_comp_eq_one_of_ker_in_range`, `MonoidHom.mulExact_iff_of_surjective_of_bijective_of_injective`, `MonoidHom.mulExact_of_comp_of_mem_range`, `MulExact.iff_monoidHom_rangeRestrict`, `MulExact.iff_of_ladder_mulEquiv`, `Submodule.mulExact_unitsMap_spanSingleton_unitsToPic`, `MonoidHom.mulExact_iff`, `Submodule.mulExact_unitsToPic_mapAlgebra`, `MonoidHom.mulExact_of_comp_eq_one_of_ker_le_range`, `MulExact.of_comp_of_mem_range`

Function.Exact

Definitions

Name	Category	Theorems
`linearEquivOfSurjective` 📖	CompOp	2 math math: `linearEquivOfSurjective_apply`, `linearEquivOfSurjective_symm_apply`
`splitInjectiveEquiv` 📖	CompOp	—
`splitSurjectiveEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addMonoidHom_comp_eq_zero` 📖	mathematical	`Function.Exact` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`AddMonoidHom.comp` `instZeroAddMonoidHom`	—	`DFunLike.coe_injective` `comp_eq_zero`
`addMonoidHom_ker_eq` 📖	mathematical	`Function.Exact` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`AddMonoidHom.ker` `AddMonoidHom.range`	—	`SetLike.ext`
`addMonoidHom_rangeRestrict` 📖	mathematical	`Function.Exact` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddMonoidHom.range` `AddSubgroup.toAddGroup` `AddSubgroup.subtype` `AddMonoidHom.rangeRestrict` `AddSubgroup.zero`	—	`iff_addMonoidHom_rangeRestrict`
`apply_apply_eq_zero` 📖	—	`Function.Exact`	—	—	`Set.mem_range_self`
`comp_eq_zero` 📖	mathematical	`Function.Exact`	`Pi.instZero`	—	`apply_apply_eq_zero`
`comp_injective` 📖	—	`Function.Exact`	—	—	—
`exact_mapQ_iff` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.comap`	`HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.mapQ` `Submodule.Quotient.instZeroQuotient` `Submodule.instMin` `LinearMap.range` `RingHomSurjective.ids` `Submodule.map`	—	`RingHomSurjective.ids` `LinearMap.exact_iff` `Submodule.comap_injective_of_surjective` `Submodule.mkQ_surjective` `RingHomCompTriple.ids` `LinearMap.ker_comp` `Submodule.range_liftQ` `Submodule.liftQ_mkQ` `LinearMap.range_comp` `Submodule.comap_map_eq` `Submodule.ker_mkQ` `linearMap_ker_eq` `sup_comm` `LE.le.ge_iff_eq'` `sup_le` `LinearMap.ker_le_comap` `Submodule.map_le_iff_le_comap` `Submodule.map_comap_eq`
`iff_addMonoidHom_rangeRestrict` 📖	mathematical	—	`Function.Exact` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddMonoidHom.range` `AddSubgroup.toAddGroup` `AddSubgroup.subtype` `AddMonoidHom.rangeRestrict` `AddSubgroup.zero`	—	`iff_rangeFactorization` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `AddSubgroup.instAddSubgroupClass`
`iff_linearMap_rangeRestrict` 📖	mathematical	—	`Function.Exact` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module` `Submodule.subtype` `LinearMap.rangeRestrict` `Submodule.zero`	—	`iff_rangeFactorization` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `RingHomSurjective.ids`
`iff_of_ladder_addEquiv` 📖	mathematical	`AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHomClass.toAddMonoidHom` `AddEquiv` `AddZero.toAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`	`Function.Exact` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddZero.toZero`	—	`AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective` `AddEquiv.surjective` `AddEquiv.bijective` `AddEquiv.injective`
`iff_of_ladder_linearEquiv` 📖	mathematical	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids`	`Function.Exact` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `iff_of_ladder_addEquiv` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`iff_rangeFactorization` 📖	mathematical	`Set` `Set.instMembership` `Set.range`	`Function.Exact` `Set.Elem` `Set.rangeFactorization`	—	`Set.mem_range` `Set.mem_range_self` `Subtype.range_coe_subtype`
`inl_snd` 📖	mathematical	—	`Function.Exact` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `LinearMap.instFunLike` `LinearMap.inl` `LinearMap.snd` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`inr_fst` 📖	mathematical	—	`Function.Exact` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `LinearMap.instFunLike` `LinearMap.inr` `LinearMap.fst` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`linearEquivOfSurjective_apply` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`LinearEquiv` `RingHomInvPair.ids` `HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `LinearMap.range` `RingHomSurjective.ids` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `linearEquivOfSurjective` `Submodule.liftQ`	—	`RingHomInvPair.ids` `RingHomSurjective.ids`
`linearEquivOfSurjective_symm_apply` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`LinearEquiv` `RingHomInvPair.ids` `HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `LinearMap.range` `RingHomSurjective.ids` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `linearEquivOfSurjective`	—	`RingHomSurjective.ids` `RingHomInvPair.ids`
`linearMap_comp_eq_zero` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`LinearMap.comp` `RingHomCompTriple.ids` `LinearMap.instZero`	—	`DFunLike.coe_injective` `RingHomCompTriple.ids` `comp_eq_zero`
`linearMap_ker_eq` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`LinearMap.ker` `LinearMap.range` `RingHomSurjective.ids`	—	`SetLike.ext` `RingHomSurjective.ids`
`linearMap_rangeRestrict` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module` `Submodule.subtype` `LinearMap.rangeRestrict` `Submodule.zero`	—	`RingHomSurjective.ids` `iff_linearMap_rangeRestrict`
`of_comp_eq_zero_of_ker_in_range` 📖	mathematical	`Pi.instZero` `Set` `Set.instMembership` `Set.range`	`Function.Exact`	—	—
`of_comp_of_mem_range` 📖	mathematical	`Pi.instZero` `Set` `Set.instMembership` `Set.range`	`Function.Exact`	—	—
`of_ladder_addEquiv_of_exact` 📖	—	`AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHomClass.toAddMonoidHom` `AddEquiv` `AddZero.toAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `Function.Exact` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddZero.toZero`	—	—	`AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `iff_of_ladder_addEquiv`
`of_ladder_addEquiv_of_exact'` 📖	—	`AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHomClass.toAddMonoidHom` `AddEquiv` `AddZero.toAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `Function.Exact` `DFunLike.coe` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddZero.toZero`	—	—	`AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `iff_of_ladder_addEquiv`
`of_ladder_linearEquiv_of_exact` 📖	—	`LinearMap.comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `Function.Exact` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `iff_of_ladder_linearEquiv`
`rangeFactorization` 📖	mathematical	`Function.Exact` `Set` `Set.instMembership` `Set.range`	`Set.Elem` `Set.rangeFactorization`	—	`iff_rangeFactorization`
`split_tfae` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`List.TFAE` `LinearMap.comp` `RingHomCompTriple.ids` `LinearMap.id` `LinearEquiv` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `LinearEquiv.toLinearMap` `LinearEquiv.symm` `LinearMap.inl` `LinearMap.snd`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `Equiv.nonempty_congr` `List.tfae_of_cycle`
`split_tfae'` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`List.TFAE` `LinearMap.comp` `RingHomCompTriple.ids` `LinearMap.id` `LinearEquiv` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `LinearEquiv.toLinearMap` `LinearEquiv.symm` `LinearMap.inl` `LinearMap.snd`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearEquiv.injective` `LinearMap.inl_injective` `Prod.snd_surjective` `Zero.instNonempty` `LinearEquiv.surjective` `List.tfae_of_cycle`

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_exact_iff_exact` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Function.Exact` `LinearMap.comp` `RingHomCompTriple.ids` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomCompTriple.ids` `map_eq_zero_iff` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`

Function.MulExact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_apply_eq_one` 📖	—	`Function.MulExact`	—	—	`Set.mem_range_self`
`comp_eq_one` 📖	mathematical	`Function.MulExact`	`Pi.instOne`	—	`apply_apply_eq_one`
`comp_injective` 📖	—	`Function.MulExact`	—	—	—
`iff_monoidHom_rangeRestrict` 📖	mathematical	—	`Function.MulExact` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `Subgroup.toGroup` `Subgroup.subtype` `MonoidHom.rangeRestrict` `Subgroup.one`	—	`iff_rangeFactorization` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass`
`iff_of_ladder_mulEquiv` 📖	mathematical	`MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`	`Function.MulExact` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike` `MulOne.toOne`	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MonoidHom.mulExact_iff_of_surjective_of_bijective_of_injective` `MulEquiv.surjective` `MulEquiv.bijective` `MulEquiv.injective`
`iff_rangeFactorization` 📖	mathematical	`Set` `Set.instMembership` `Set.range`	`Function.MulExact` `Set.Elem` `Set.rangeFactorization`	—	`Set.mem_range_self` `Subtype.range_coe_subtype`
`monoidHom_comp_eq_zero` 📖	mathematical	`Function.MulExact` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`MonoidHom.comp` `instOneMonoidHom`	—	`DFunLike.coe_injective` `comp_eq_one`
`monoidHom_ker_eq` 📖	mathematical	`Function.MulExact` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`MonoidHom.ker` `MonoidHom.range`	—	`SetLike.ext`
`monoidHom_rangeRestrict` 📖	mathematical	`Function.MulExact` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `Subgroup.toGroup` `Subgroup.subtype` `MonoidHom.rangeRestrict` `Subgroup.one`	—	`iff_monoidHom_rangeRestrict`
`of_comp_eq_one_of_ker_in_range` 📖	mathematical	`Pi.instOne` `Set` `Set.instMembership` `Set.range`	`Function.MulExact`	—	—
`of_comp_of_mem_range` 📖	mathematical	`Pi.instOne` `Set` `Set.instMembership` `Set.range`	`Function.MulExact`	—	—
`of_ladder_mulEquiv_of_mulExact` 📖	—	`MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `Function.MulExact` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike` `MulOne.toOne`	—	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `iff_of_ladder_mulEquiv`
`of_ladder_mulEquiv_of_mulExact'` 📖	—	`MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `Function.MulExact` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike` `MulOne.toOne`	—	—	`MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `iff_of_ladder_mulEquiv`
`rangeFactorization` 📖	mathematical	`Function.MulExact` `Set` `Set.instMembership` `Set.range`	`Set.Elem` `Set.rangeFactorization`	—	`iff_rangeFactorization`

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_exact_iff_exact` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Function.Exact` `LinearMap.comp` `RingHomCompTriple.ids` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomCompTriple.ids` `range_comp`

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conj_exact_iff_exact` 📖	mathematical	—	`Function.Exact` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `LinearMap.comp` `RingHomCompTriple.ids` `toLinearMap` `RingHomInvPair.ids` `symm` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `RingHomSurjective.ids` `RingHomSurjective.invPair` `LinearMap.range_comp` `Submodule.map_injective_of_injective` `injective`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact_iff` 📖	mathematical	—	`Function.Exact` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `ker` `range` `RingHomSurjective.ids`	—	`RingHomSurjective.ids` `SetLike.ext_iff`
`exact_iff_of_surjective_of_bijective_of_injective` 📖	mathematical	`comp` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `LinearMap` `instFunLike` `Function.Bijective`	`Function.Exact` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomCompTriple.ids` `AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective` `AddMonoidHom.ext` `DFunLike.congr_fun`
`exact_map_mkQ_range` 📖	mathematical	—	`Function.Exact` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `DFunLike.coe` `LinearMap` `instFunLike` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.mkQ` `Submodule.Quotient.instZeroQuotient`	—	`RingHomSurjective.ids` `exact_iff` `Submodule.ker_mkQ`
`exact_of_comp_eq_zero_of_ker_le_range` 📖	mathematical	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap` `instZero` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `ker` `range` `RingHomSurjective.ids`	`Function.Exact` `DFunLike.coe` `instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomCompTriple.ids` `RingHomSurjective.ids` `Function.Exact.of_comp_of_mem_range`
`exact_of_comp_of_mem_range` 📖	mathematical	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap` `instZero` `Submodule` `SetLike.instMembership` `Submodule.setLike` `range` `RingHomSurjective.ids`	`Function.Exact` `DFunLike.coe` `instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomCompTriple.ids` `RingHomSurjective.ids` `exact_of_comp_eq_zero_of_ker_le_range`
`exact_subtype_ker_map` 📖	mathematical	—	`Function.Exact` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `ker` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearMap` `Submodule.addCommMonoid` `Submodule.module` `instFunLike` `Submodule.subtype` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomSurjective.ids` `exact_iff` `Submodule.range_subtype`
`exact_subtype_mkQ` 📖	mathematical	—	`Function.Exact` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `HasQuotient.Quotient` `Submodule.hasQuotient` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `Submodule.module` `instFunLike` `Submodule.subtype` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.mkQ` `Submodule.Quotient.instZeroQuotient`	—	`RingHomSurjective.ids` `exact_iff` `Submodule.ker_mkQ` `Submodule.range_subtype`
`exact_zero_iff_injective` 📖	mathematical	—	`Function.Exact` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomSurjective.ids` `range_zero`
`exact_zero_iff_surjective` 📖	mathematical	—	`Function.Exact` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomSurjective.ids` `ker_zero`
`injective_range_liftQ_of_exact` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `range` `RingHomSurjective.ids` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.liftQ` `Set` `Set.instMembership` `Set.range`	—	`RingHomSurjective.ids`
`ker_eq_bot_range_liftQ_iff` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ker`	`HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.liftQ` `Bot.bot` `Submodule.instBot`	—	`RingHomSurjective.ids` `Submodule.Quotient.mk_surjective`
`surjective_range_liftQ` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ker` `DFunLike.coe` `LinearMap` `instFunLike`	`HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.liftQ`	—	`RingHomSurjective.ids`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulExact_iff` 📖	mathematical	—	`Function.MulExact` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `ker` `range`	—	`SetLike.ext_iff`
`mulExact_iff_of_surjective_of_bijective_of_injective` 📖	mathematical	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `DFunLike.coe` `MonoidHom` `instFunLike` `Function.Bijective`	`Function.MulExact` `MulOne.toOne`	—	`DFunLike.congr_fun` `map_one` `MonoidHomClass.toOneHomClass` `instMonoidHomClass` `Function.MulExact.apply_apply_eq_one`
`mulExact_of_comp_eq_one_of_ker_le_range` 📖	mathematical	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom` `instOneMonoidHom` `Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `ker` `range`	`Function.MulExact` `DFunLike.coe` `instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Function.MulExact.of_comp_of_mem_range`
`mulExact_of_comp_of_mem_range` 📖	mathematical	`comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom` `instOneMonoidHom` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `range`	`Function.MulExact` `DFunLike.coe` `instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mulExact_of_comp_eq_one_of_ker_le_range`

---

← Back to Index