Mathlib Map

Theorems · Theorem · group theory

MonoidHom.card_fiber_eq_of_mem_range

∀ {G : Type u_1} {M : Type u_2} {F : Type u_3} [inst : Group G] [inst_1 : Fintype G] [inst_2 : Monoid M]
  [inst_3 : DecidableEq M] [inst_4 : FunLike F G M] [MonoidHomClass F G M] (f : F) {x y : M},
  x ∈ Set.range ⇑f → y ∈ Set.range ⇑f → {g | f g = x}.card = {g | f g = y}.card
Defined in
Mathlib.GroupTheory.Index
Cited by
1 results in Mathlib
Foundations
Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
GroupFintypeMonoidDecidableEqFunLikeMonoidHomClass
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

sum_hom_units_eq_zero · cited by 1sum_hom_units_eq_zeroDFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetFinset · cited by 13712FinsetFintype · cited by 7736FintypeGroup · cited by 6238GroupSet.range · cited by 4705Set.rangeMonoid · cited by 3887MonoidMonoidHom · cited by 3629MonoidHomFinset.univ · cited by 3473Finset.univUnits · cited by 2804UnitsFunLike · cited by 2560FunLikeFinset.card · cited by 2327Finset.cardUnits.val · cited by 1966Units.valmap_mul · cited by 1137map_mulFinset.filter · cited by 949Finset.filterMonoidHom.card_fiber_eq_of_me…CITED BYCITES

Cites27

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • DFunLike.coestatement and proof · cited by 62,936
  • Setstatement · cited by 53,352
  • Finsetproof · cited by 13,712
  • Fintypestatement and proof · cited by 7,736
  • Groupstatement and proof · cited by 6,238
  • Set.rangestatement and proof · cited by 4,705
  • Monoidstatement and proof · cited by 3,887
  • MonoidHomproof · cited by 3,629
  • Finset.univstatement and proof · cited by 3,473
  • Unitsproof · cited by 2,804
  • FunLikestatement and proof · cited by 2,560
  • Finset.cardstatement and proof · cited by 2,327

Cited by1

Results whose statement or proof uses this declaration.