Documentation Verification Report

EpiMono

📁 Source: Mathlib/Algebra/Category/Grp/EpiMono.lean

Statistics

Metric	Count
Definitions `XWithInfinity`, `g`, `h`, `instDecidableEqXWithInfinity`, `instSMulCarrierXWithInfinity`, `tau`	6
Theorems `epi_iff_range_eq_top`, `epi_iff_surjective`, `forget_commGrp_preserves_epi`, `forget_commGrp_preserves_mono`, `ker_eq_bot_of_mono`, `mono_iff_injective`, `mono_iff_ker_eq_bot`, `range_eq_top_of_epi`, `epi_iff_range_eq_top`, `epi_iff_surjective`, `forget_grp_preserves_epi`, `forget_grp_preserves_mono`, `ker_eq_bot_of_mono`, `mono_iff_injective`, `mono_iff_ker_eq_bot`, `ker_eq_bot_of_cancel`, `range_eq_top_of_cancel`, `epi_iff_range_eq_top`, `epi_iff_surjective`, `forget_commGrp_preserves_epi`, `forget_commGrp_preserves_mono`, `ker_eq_bot_of_mono`, `mono_iff_injective`, `mono_iff_ker_eq_bot`, `range_eq_top_of_epi`, `agree`, `comp_eq`, `fromCoset_eq_of_mem_range`, `fromCoset_ne_of_nin_range`, `g_apply_fromCoset`, `g_apply_infinity`, `g_ne_h`, `h_apply_fromCoset`, `h_apply_fromCoset'`, `h_apply_fromCoset_nin_range`, `h_apply_infinity`, `mul_smul`, `one_smul`, `τ_apply_fromCoset`, `τ_apply_fromCoset'`, `τ_apply_infinity`, `τ_symm_apply_fromCoset`, `τ_symm_apply_infinity`, `epi_iff_range_eq_top`, `epi_iff_surjective`, `forget_grp_preserves_epi`, `forget_grp_preserves_mono`, `ker_eq_bot_of_mono`, `mono_iff_injective`, `mono_iff_ker_eq_bot`, `surjective_of_epi`, `ker_eq_bot_of_cancel`, `range_eq_top_of_cancel`	53
Total	59

AddCommGrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_range_eq_top` 📖	mathematical	—	`CategoryTheory.Epi` `AddCommGrpCat` `instCategory` `AddMonoidHom.range` `carrier` `AddCommGroup.toAddGroup` `str` `Hom.hom` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	—	`range_eq_top_of_epi` `CategoryTheory.ConcreteCategory.epi_of_surjective` `AddMonoidHom.range_eq_top`
`epi_iff_surjective` 📖	mathematical	—	`CategoryTheory.Epi` `AddCommGrpCat` `instCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`epi_iff_range_eq_top` `AddMonoidHom.range_eq_top`
`forget_commGrp_preserves_epi` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms` `AddCommGrpCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`CategoryTheory.epi_iff_surjective` `epi_iff_surjective`
`forget_commGrp_preserves_mono` 📖	mathematical	—	`CategoryTheory.Functor.PreservesMonomorphisms` `AddCommGrpCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`CategoryTheory.mono_iff_injective` `mono_iff_injective`
`ker_eq_bot_of_mono` 📖	mathematical	—	`AddMonoidHom.ker` `carrier` `AddCommGroup.toAddGroup` `str` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Hom.hom` `Bot.bot` `AddSubgroup` `AddSubgroup.instBot`	—	`AddMonoidHom.ker_eq_bot_of_cancel` `CategoryTheory.ConcreteCategory.ext_iff` `CategoryTheory.cancel_mono` `CategoryTheory.ConcreteCategory.ext`
`mono_iff_injective` 📖	mathematical	—	`CategoryTheory.Mono` `AddCommGrpCat` `instCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`mono_iff_ker_eq_bot` `AddMonoidHom.ker_eq_bot_iff`
`mono_iff_ker_eq_bot` 📖	mathematical	—	`CategoryTheory.Mono` `AddCommGrpCat` `instCategory` `AddMonoidHom.ker` `carrier` `AddCommGroup.toAddGroup` `str` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Hom.hom` `Bot.bot` `AddSubgroup` `AddSubgroup.instBot`	—	`ker_eq_bot_of_mono` `CategoryTheory.ConcreteCategory.mono_of_injective` `AddMonoidHom.ker_eq_bot_iff`
`range_eq_top_of_epi` 📖	mathematical	—	`AddMonoidHom.range` `carrier` `AddCommGroup.toAddGroup` `str` `Hom.hom` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	—	`AddMonoidHom.range_eq_top_of_cancel` `AddSubgroup.normal_of_comm` `CategoryTheory.ConcreteCategory.ext_iff` `CategoryTheory.cancel_epi` `CategoryTheory.ConcreteCategory.ext`

AddGrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_range_eq_top` 📖	mathematical	—	`CategoryTheory.Epi` `AddGrpCat` `instCategory` `AddMonoidHom.range` `carrier` `str` `Hom.hom` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	—	`epi_iff_surjective` `AddSubgroup.eq_top_iff'`
`epi_iff_surjective` 📖	mathematical	—	`CategoryTheory.Epi` `AddGrpCat` `instCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`CategoryTheory.Functor.map_epi` `CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_inverse` `CategoryTheory.Functor.epi_of_epi_map` `CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape` `CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsColimits` `CategoryTheory.Limits.fullyFaithful_reflectsColimits` `CategoryTheory.Equivalence.full_inverse` `CategoryTheory.Equivalence.faithful_inverse` `GrpCat.epi_iff_surjective`
`forget_grp_preserves_epi` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms` `AddGrpCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`CategoryTheory.epi_iff_surjective` `epi_iff_surjective`
`forget_grp_preserves_mono` 📖	mathematical	—	`CategoryTheory.Functor.PreservesMonomorphisms` `AddGrpCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`CategoryTheory.mono_iff_injective` `mono_iff_injective`
`ker_eq_bot_of_mono` 📖	mathematical	—	`AddMonoidHom.ker` `carrier` `str` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Hom.hom` `Bot.bot` `AddSubgroup` `AddSubgroup.instBot`	—	`AddMonoidHom.ker_eq_bot_of_cancel` `CategoryTheory.ConcreteCategory.ext_iff` `CategoryTheory.cancel_mono` `CategoryTheory.ConcreteCategory.ext`
`mono_iff_injective` 📖	mathematical	—	`CategoryTheory.Mono` `AddGrpCat` `instCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`mono_iff_ker_eq_bot` `AddMonoidHom.ker_eq_bot_iff`
`mono_iff_ker_eq_bot` 📖	mathematical	—	`CategoryTheory.Mono` `AddGrpCat` `instCategory` `AddMonoidHom.ker` `carrier` `str` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Hom.hom` `Bot.bot` `AddSubgroup` `AddSubgroup.instBot`	—	`ker_eq_bot_of_mono` `CategoryTheory.ConcreteCategory.mono_of_injective` `AddMonoidHom.ker_eq_bot_iff`

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_eq_bot_of_cancel` 📖	mathematical	—	`ker` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Bot.bot` `AddSubgroup` `AddSubgroup.instBot`	—	`AddSubgroup.range_subtype` `range_zero` `comp_zero` `ext` `mem_ker`
`range_eq_top_of_cancel` 📖	mathematical	—	`range` `AddCommGroup.toAddGroup` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	—	`AddSubgroup.normal_of_comm` `ext` `QuotientAddGroup.mk_zero` `QuotientAddGroup.eq` `neg_zero` `zero_add` `QuotientAddGroup.ker_mk'` `ker_zero`

CommGrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_range_eq_top` 📖	mathematical	—	`CategoryTheory.Epi` `CommGrpCat` `instCategory` `MonoidHom.range` `carrier` `CommGroup.toGroup` `str` `Hom.hom` `Top.top` `Subgroup` `Subgroup.instTop`	—	`range_eq_top_of_epi` `CategoryTheory.ConcreteCategory.epi_of_surjective` `MonoidHom.range_eq_top`
`epi_iff_surjective` 📖	mathematical	—	`CategoryTheory.Epi` `CommGrpCat` `instCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`epi_iff_range_eq_top` `MonoidHom.range_eq_top`
`forget_commGrp_preserves_epi` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms` `CommGrpCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`CategoryTheory.epi_iff_surjective` `epi_iff_surjective`
`forget_commGrp_preserves_mono` 📖	mathematical	—	`CategoryTheory.Functor.PreservesMonomorphisms` `CommGrpCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`CategoryTheory.mono_iff_injective` `mono_iff_injective`
`ker_eq_bot_of_mono` 📖	mathematical	—	`MonoidHom.ker` `carrier` `CommGroup.toGroup` `str` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Hom.hom` `Bot.bot` `Subgroup` `Subgroup.instBot`	—	`MonoidHom.ker_eq_bot_of_cancel` `CategoryTheory.ConcreteCategory.ext_iff` `CategoryTheory.cancel_mono` `CategoryTheory.ConcreteCategory.ext`
`mono_iff_injective` 📖	mathematical	—	`CategoryTheory.Mono` `CommGrpCat` `instCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`mono_iff_ker_eq_bot` `MonoidHom.ker_eq_bot_iff`
`mono_iff_ker_eq_bot` 📖	mathematical	—	`CategoryTheory.Mono` `CommGrpCat` `instCategory` `MonoidHom.ker` `carrier` `CommGroup.toGroup` `str` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Hom.hom` `Bot.bot` `Subgroup` `Subgroup.instBot`	—	`ker_eq_bot_of_mono` `CategoryTheory.ConcreteCategory.mono_of_injective` `MonoidHom.ker_eq_bot_iff`
`range_eq_top_of_epi` 📖	mathematical	—	`MonoidHom.range` `carrier` `CommGroup.toGroup` `str` `Hom.hom` `Top.top` `Subgroup` `Subgroup.instTop`	—	`MonoidHom.range_eq_top_of_cancel` `Subgroup.normal_of_comm` `CategoryTheory.ConcreteCategory.ext_iff` `CategoryTheory.cancel_epi` `CategoryTheory.ConcreteCategory.ext`

GrpCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_range_eq_top` 📖	mathematical	—	`CategoryTheory.Epi` `GrpCat` `instCategory` `MonoidHom.range` `carrier` `str` `Hom.hom` `Top.top` `Subgroup` `Subgroup.instTop`	—	`epi_iff_surjective` `Subgroup.eq_top_iff'`
`epi_iff_surjective` 📖	mathematical	—	`CategoryTheory.Epi` `GrpCat` `instCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`surjective_of_epi` `CategoryTheory.ConcreteCategory.epi_of_surjective`
`forget_grp_preserves_epi` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms` `GrpCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`CategoryTheory.epi_iff_surjective` `epi_iff_surjective`
`forget_grp_preserves_mono` 📖	mathematical	—	`CategoryTheory.Functor.PreservesMonomorphisms` `GrpCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`CategoryTheory.mono_iff_injective` `mono_iff_injective`
`ker_eq_bot_of_mono` 📖	mathematical	—	`MonoidHom.ker` `carrier` `str` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Hom.hom` `Bot.bot` `Subgroup` `Subgroup.instBot`	—	`MonoidHom.ker_eq_bot_of_cancel` `CategoryTheory.ConcreteCategory.ext_iff` `CategoryTheory.cancel_mono` `CategoryTheory.ConcreteCategory.ext`
`mono_iff_injective` 📖	mathematical	—	`CategoryTheory.Mono` `GrpCat` `instCategory` `carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`mono_iff_ker_eq_bot` `MonoidHom.ker_eq_bot_iff`
`mono_iff_ker_eq_bot` 📖	mathematical	—	`CategoryTheory.Mono` `GrpCat` `instCategory` `MonoidHom.ker` `carrier` `str` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Hom.hom` `Bot.bot` `Subgroup` `Subgroup.instBot`	—	`ker_eq_bot_of_mono` `CategoryTheory.ConcreteCategory.mono_of_injective` `MonoidHom.ker_eq_bot_iff`
`surjective_of_epi` 📖	mathematical	—	`carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `GrpCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`Mathlib.Tactic.Push.not_forall_eq` `SurjectiveOfEpiAuxs.g_ne_h` `CategoryTheory.cancel_epi` `SurjectiveOfEpiAuxs.comp_eq`

GrpCat.SurjectiveOfEpiAuxs

Definitions

Name	Category	Theorems
`XWithInfinity` 📖	CompData	15 math math: `τ_apply_fromCoset`, `τ_symm_apply_infinity`, `τ_apply_infinity`, `g_apply_infinity`, `comp_eq`, `agree`, `h_apply_fromCoset'`, `h_apply_infinity`, `h_apply_fromCoset`, `h_apply_fromCoset_nin_range`, `mul_smul`, `g_apply_fromCoset`, `τ_symm_apply_fromCoset`, `one_smul`, `τ_apply_fromCoset'`
`g` 📖	CompOp	4 math math: `g_apply_infinity`, `comp_eq`, `agree`, `g_apply_fromCoset`
`h` 📖	CompOp	6 math math: `comp_eq`, `agree`, `h_apply_fromCoset'`, `h_apply_infinity`, `h_apply_fromCoset`, `h_apply_fromCoset_nin_range`
`instDecidableEqXWithInfinity` 📖	CompOp	—
`instSMulCarrierXWithInfinity` 📖	CompOp	2 math math: `mul_smul`, `one_smul`
`tau` 📖	CompOp	5 math math: `τ_apply_fromCoset`, `τ_symm_apply_infinity`, `τ_apply_infinity`, `τ_symm_apply_fromCoset`, `τ_apply_fromCoset'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`agree` 📖	mathematical	—	`SetLike.coe` `Subgroup` `GrpCat.carrier` `GrpCat.str` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom` `setOf` `Equiv.Perm` `XWithInfinity` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `h` `g`	—	`Set.ext` `Equiv.Perm.ext` `g_apply_fromCoset` `h_apply_fromCoset'` `one_leftCoset` `fromCoset_eq_of_mem_range` `smul_smul` `Subgroup.mul_mem` `h_apply_fromCoset_nin_range` `leftCoset_assoc` `g_apply_infinity` `h_apply_infinity` `by_contradiction` `Equiv.swap_apply_left` `Equiv.swap_apply_right` `fromCoset_ne_of_nin_range` `DFunLike.congr_fun`
`comp_eq` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `GrpCat` `CategoryTheory.Category.toCategoryStruct` `GrpCat.instCategory` `GrpCat.of` `Equiv.Perm` `XWithInfinity` `Equiv.Perm.permGroup` `GrpCat.ofHom` `GrpCat.carrier` `GrpCat.str` `g` `h`	—	`GrpCat.hom_ext` `MonoidHom.ext` `Equiv.Perm.ext` `agree`
`fromCoset_eq_of_mem_range` 📖	mathematical	`GrpCat.carrier` `Subgroup` `GrpCat.str` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom`	`XWithInfinity.fromCoset` `Set` `Set.instMembership` `Set.range` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `one_leftCoset` `DivInvOneMonoid.toDivInvMonoid`	—	`one_leftCoset` `leftCoset_eq_iff` `mul_one` `Subgroup.inv_mem`
`fromCoset_ne_of_nin_range` 📖	—	`GrpCat.carrier` `Subgroup` `GrpCat.str` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom`	—	—	`one_leftCoset` `Subgroup.inv_mem` `mul_one` `leftCoset_eq_iff` `inv_inv`
`g_apply_fromCoset` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `XWithInfinity` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `GrpCat.carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `g` `XWithInfinity.fromCoset` `Set` `Set.instMembership` `Set.range` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom`	—	—
`g_apply_infinity` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `XWithInfinity` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `GrpCat.carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `g` `XWithInfinity.infinity`	—	—
`g_ne_h` 📖	—	`GrpCat.carrier` `Subgroup` `GrpCat.str` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom`	—	—	`fromCoset_ne_of_nin_range` `one_leftCoset` `DFunLike.congr_fun` `Equiv.swap_apply_left` `Equiv.swap_apply_right`
`h_apply_fromCoset` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `XWithInfinity` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `GrpCat.carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `h` `XWithInfinity.fromCoset` `Set` `Set.instMembership` `Set.range` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `one_leftCoset` `DivInvOneMonoid.toDivInvMonoid`	—	`one_leftCoset` `τ_symm_apply_fromCoset` `τ_apply_infinity`
`h_apply_fromCoset'` 📖	mathematical	`GrpCat.carrier` `Subgroup` `GrpCat.str` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom`	`DFunLike.coe` `Equiv.Perm` `XWithInfinity` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `h` `XWithInfinity.fromCoset` `Set` `Set.instMembership` `Set.range` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe`	—	`one_leftCoset` `h_apply_fromCoset` `fromCoset_eq_of_mem_range`
`h_apply_fromCoset_nin_range` 📖	mathematical	`GrpCat.carrier` `Subgroup` `GrpCat.str` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom`	`DFunLike.coe` `Equiv.Perm` `XWithInfinity` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `h` `XWithInfinity.fromCoset` `Set` `Set.instMembership` `Set.range` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `MulOne.toMul`	—	`Equiv.symm_swap` `one_leftCoset` `Equiv.swap_apply_of_ne_of_ne` `fromCoset_ne_of_nin_range` `leftCoset_assoc` `mul_assoc` `inv_mul_cancel` `one_mul` `Subgroup.mul_mem` `Subgroup.inv_mem`
`h_apply_infinity` 📖	mathematical	`GrpCat.carrier` `Subgroup` `GrpCat.str` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom`	`DFunLike.coe` `Equiv.Perm` `XWithInfinity` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `h` `XWithInfinity.infinity`	—	`one_leftCoset` `τ_symm_apply_infinity` `g_apply_fromCoset` `τ_apply_fromCoset'`
`mul_smul` 📖	mathematical	—	`GrpCat.carrier` `XWithInfinity` `instSMulCarrierXWithInfinity` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str`	—	`leftCoset_assoc`
`one_smul` 📖	mathematical	—	`GrpCat.carrier` `XWithInfinity` `instSMulCarrierXWithInfinity` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `GrpCat.str`	—	`one_leftCoset`
`τ_apply_fromCoset` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `XWithInfinity` `EquivLike.toFunLike` `Equiv.instEquivLike` `tau` `XWithInfinity.fromCoset` `Set` `GrpCat.carrier` `Set.instMembership` `Set.range` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `one_leftCoset` `DivInvOneMonoid.toDivInvMonoid` `XWithInfinity.infinity`	—	`Equiv.swap_apply_left`
`τ_apply_fromCoset'` 📖	mathematical	`GrpCat.carrier` `Subgroup` `GrpCat.str` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom`	`DFunLike.coe` `Equiv.Perm` `XWithInfinity` `EquivLike.toFunLike` `Equiv.instEquivLike` `tau` `XWithInfinity.fromCoset` `Set` `Set.instMembership` `Set.range` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `XWithInfinity.infinity`	—	`one_leftCoset` `τ_apply_fromCoset` `fromCoset_eq_of_mem_range`
`τ_apply_infinity` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `XWithInfinity` `EquivLike.toFunLike` `Equiv.instEquivLike` `tau` `XWithInfinity.infinity` `XWithInfinity.fromCoset` `Set` `GrpCat.carrier` `Set.instMembership` `Set.range` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `one_leftCoset` `DivInvOneMonoid.toDivInvMonoid`	—	`Equiv.swap_apply_right`
`τ_symm_apply_fromCoset` 📖	mathematical	—	`DFunLike.coe` `Equiv` `XWithInfinity` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `tau` `XWithInfinity.fromCoset` `Set` `GrpCat.carrier` `Set.instMembership` `Set.range` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `one_leftCoset` `DivInvOneMonoid.toDivInvMonoid` `XWithInfinity.infinity`	—	`one_leftCoset` `tau.eq_1` `Equiv.symm_swap` `Equiv.swap_apply_left`
`τ_symm_apply_infinity` 📖	mathematical	—	`DFunLike.coe` `Equiv` `XWithInfinity` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `tau` `XWithInfinity.infinity` `XWithInfinity.fromCoset` `Set` `GrpCat.carrier` `Set.instMembership` `Set.range` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `MulAction.toSemigroupAction` `Monoid.toMulAction` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MonoidHom.range` `GrpCat.Hom.hom` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `one_leftCoset` `DivInvOneMonoid.toDivInvMonoid`	—	`one_leftCoset` `tau.eq_1` `Equiv.symm_swap` `Equiv.swap_apply_right`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_eq_bot_of_cancel` 📖	mathematical	—	`ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Bot.bot` `Subgroup` `Subgroup.instBot`	—	`Subgroup.range_subtype` `range_one` `comp_one` `ext`
`range_eq_top_of_cancel` 📖	mathematical	—	`range` `CommGroup.toGroup` `Top.top` `Subgroup` `Subgroup.instTop`	—	`Subgroup.normal_of_comm` `ext` `QuotientGroup.mk_one` `QuotientGroup.eq` `inv_one` `one_mul` `QuotientGroup.ker_mk'` `ker_one`

---

← Back to Index