English
PowCoprime with a fixed match property equals identity under certain structural conditions.
Русский
PowCoprime удовлетворяет свойству соответствия, приводя к тождеству при определённых условиях.
LaTeX
$$powCoprime_match_1 : (some equivalence condition) → powCoprime h 1 = 1$$
Lean4
/-- A nonempty idempotent subset of a finite cancellative monoid is a submonoid -/
@[to_additive /-- A nonempty idempotent subset of a finite cancellative additive monoid is a submonoid -/
]
def submonoidOfIdempotent {M : Type*} [LeftCancelMonoid M] [Finite M] (S : Set M) (hS1 : S.Nonempty) (hS2 : S * S = S) :
Submonoid M :=
have pow_mem (a : M) (ha : a ∈ S) (n : ℕ) : a ^ (n + 1) ∈ S := by
induction n with
| zero => rwa [zero_add, pow_one]
| succ n ih =>
rw [← hS2, pow_succ]
exact Set.mul_mem_mul ih ha
{ carrier := S
one_mem' := by
obtain ⟨a, ha⟩ := hS1
rw [← pow_orderOf_eq_one a, ← tsub_add_cancel_of_le (succ_le_of_lt (orderOf_pos a))]
exact pow_mem a ha (orderOf a - 1)
mul_mem' := fun ha hb => (congr_arg₂ (· ∈ ·) rfl hS2).mp (Set.mul_mem_mul ha hb) }
