English
If φ has constantCoeff φ = u, then φ · invOfUnit φ u = 1.
Русский
Если константный коэффициент φ равен u, то φ · invOfUnit φ u = 1.
LaTeX
$$$ φ \cdot \mathrm{invOfUnit}(φ, u) = 1 $$$
Lean4
@[simp]
theorem mul_invOfUnit (φ : MvPowerSeries σ R) (u : Rˣ) (h : constantCoeff φ = u) : φ * invOfUnit φ u = 1 :=
ext fun n =>
letI := Classical.decEq (σ →₀ ℕ)
if H : n = 0 then by
rw [H]
simp [h]
else by
classical
have : ((0 : σ →₀ ℕ), n) ∈ antidiagonal n := by rw [mem_antidiagonal, zero_add]
rw [coeff_one, if_neg H, coeff_mul, ← Finset.insert_erase this, Finset.sum_insert (Finset.notMem_erase _ _),
coeff_zero_eq_constantCoeff_apply, h, coeff_invOfUnit, if_neg H, neg_mul, mul_neg, Units.mul_inv_cancel_left, ←
Finset.insert_erase this, Finset.sum_insert (Finset.notMem_erase _ _), Finset.insert_erase this,
if_neg (not_lt_of_ge <| le_rfl), zero_add, add_comm, ← sub_eq_add_neg, sub_eq_zero, Finset.sum_congr rfl]
rintro ⟨i, j⟩ hij
rw [Finset.mem_erase, mem_antidiagonal] at hij
obtain ⟨h₁, h₂⟩ := hij
subst n
rw [if_pos]
suffices 0 + j < i + j by simpa
apply add_lt_add_right
constructor
· intro s
exact Nat.zero_le _
· intro H
apply h₁
suffices i = 0 by simp [this]
ext1 s
exact
Nat.eq_zero_of_le_zero
(H s)
-- TODO : can one prove equivalence?
