English
Eq (powCoprime h) (Eq One) under some normal form; i.e., properties of equivalence mapping.
Русский
Эквивалентность powCoprime к единице в особых условиях.
LaTeX
$$powCoprime_eq_one : powCoprime h 1 = 1$$
Lean4
/-- If `S` is a nonempty subset of a finite group `G`, then `S ^ |G|` is a subgroup -/
@[to_additive (attr := simps!) smulCardAddSubgroup /--
If `S` is a nonempty subset of a finite additive group `G`, then `|G| • S` is a subgroup -/
]
def powCardSubgroup {G : Type*} [Group G] [Fintype G] (S : Set G) (hS : S.Nonempty) : Subgroup G :=
have one_mem : (1 : G) ∈ S ^ Fintype.card G := by
obtain ⟨a, ha⟩ := hS
rw [← pow_card_eq_one]
exact Set.pow_mem_pow ha
subgroupOfIdempotent (S ^ Fintype.card G) ⟨1, one_mem⟩ <| by
classical
apply (Set.eq_of_subset_of_card_le (Set.subset_mul_left _ one_mem) (ge_of_eq _)).symm
simp_rw [← pow_add, Group.card_pow_eq_card_pow_card_univ S (Fintype.card G + Fintype.card G) le_add_self]
