QuotientInter

📁 Source: Mathlib/Geometry/Group/Growth/QuotientInter.lean

Statistics

Metric	Count
Definitions	0
Theorems card_nsmul_quotient_add_nsmul_inter_addSubgroup_le, card_pow_quotient_mul_pow_inter_subgroup_le, le_card_quotient_add_sq_inter_addSubgroup, le_card_quotient_mul_sq_inter_subgroup	4
Total	4

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_nsmul_quotient_add_nsmul_inter_addSubgroup_le 📖	mathematical	—	card HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup image QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddMonoidHom.instFunLike QuotientAddGroup.mk' Finset nsmul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddZero.toAdd filter SetLike.instMembership AddSubgroup.instSetLike	—	Zero.instNonempty Function.invFunOn_injOn_image Function.invFunOn_mem Set.mem_image Function.invFunOn.congr_simp coe_nsmul mem_coe Function.invFunOn_eq card_image_of_injOn coe_image card_add_iff coe_filter Set.mem_prod exists_exists_and_eq_and QuotientAddGroup.eq_zero_iff map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass Set.mem_image_of_mem add_zero AddLeftCancelSemigroup.toIsLeftCancelAdd le_refl card_le_card add_nsmul add_subset_iff mem_image mem_filter add_mem_add
card_pow_quotient_mul_pow_inter_subgroup_le 📖	mathematical	—	card HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup image QuotientGroup.instDecidableEqQuotientSubgroupOfDecidablePredMem DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group MonoidHom.instFunLike QuotientGroup.mk' Finset npow InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid MulOne.toMul filter SetLike.instMembership Subgroup.instSetLike	—	One.instNonempty Function.invFunOn_injOn_image Function.invFunOn_mem Function.invFunOn.congr_simp coe_pow Function.invFunOn_eq card_image_of_injOn card_mul_iff coe_image coe_filter QuotientGroup.eq_one_iff map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass Set.mem_image_of_mem mul_one LeftCancelSemigroup.toIsLeftCancelMul le_refl card_le_card pow_add mul_mem_mul
le_card_quotient_add_sq_inter_addSubgroup 📖	mathematical	Finset neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	card HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup image QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddMonoidHom.instFunLike QuotientAddGroup.mk' filter SetLike.instMembership AddSubgroup.instSetLike AddMonoid.toNatSMul addMonoid	—	card_eq_sum_card_image sum_le_card_nsmul IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid forall_mem_image card_le_card_add_left AddLeftCancelSemigroup.toIsLeftCancelAdd neg_filter filter.congr_simp map_neg AddMonoidHom.instAddMonoidHomClass mem_filter mem_neg' neg_neg card_le_card add_subset_iff add_mem_add QuotientAddGroup.eq_zero_iff map_add AddMonoidHomClass.toAddHomClass add_neg_cancel two_nsmul
le_card_quotient_mul_sq_inter_subgroup 📖	mathematical	Finset inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	card HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup image QuotientGroup.instDecidableEqQuotientSubgroupOfDecidablePredMem DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group MonoidHom.instFunLike QuotientGroup.mk' filter SetLike.instMembership Subgroup.instSetLike Monoid.toNatPow monoid	—	card_eq_sum_card_image sum_le_card_nsmul IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid forall_mem_image card_le_card_mul_left LeftCancelSemigroup.toIsLeftCancelMul inv_filter filter.congr_simp map_inv MonoidHom.instMonoidHomClass inv_inv card_le_card mul_mem_mul QuotientGroup.eq_one_iff map_mul MonoidHomClass.toMulHomClass mul_inv_cancel sq

---

← Back to Index