English
If (x − x^2)^n = 0, then 1 − (1 − x^n)^n is idempotent.
Русский
Если (x − x^2)^n = 0, то 1 − (1 − x^n)^n является идемпотентом.
LaTeX
$$IsIdempotentElem\big(1 - (1 - x^n)^n\big)$$
Lean4
theorem isIdempotentElem_one_sub_one_sub_pow_pow (x : R) (n : ℕ) (hx : (x - x ^ 2) ^ n = 0) :
IsIdempotentElem (1 - (1 - x ^ n) ^ n) :=
by
have : (x - x ^ 2) ^ n ∣ (1 - (1 - x ^ n) ^ n) - (1 - (1 - x ^ n) ^ n) ^ 2 :=
by
conv_rhs => rw [pow_two, ← mul_one_sub, sub_sub_cancel]
nth_rw 1 3 [← one_pow n]
rw [← (Commute.one_left x).mul_geom_sum₂, ← (Commute.one_left (1 - x ^ n)).mul_geom_sum₂]
simp only [sub_sub_cancel, one_pow, one_mul]
rw [Commute.mul_pow, Commute.mul_mul_mul_comm, ← Commute.mul_pow, mul_one_sub, ← pow_two]
· exact ⟨_, rfl⟩
· simp
· refine .pow_right (.sub_right (.one_right _) (.sum_left _ _ _ fun _ _ ↦ .pow_left ?_ _)) _
simp
· exact .sub_left (.one_left _) (.sum_right _ _ _ fun _ _ ↦ .pow_right rfl _)
rwa [hx, zero_dvd_iff, sub_eq_zero, eq_comm, pow_two] at this
