English
There exists a field structure on HahnSeries Γ R extending the base field structure, with specified inverses and scalars, making HahnSeries a field.
Русский
Существует структура поля на HahnSeries Γ R, расширяющая базовую структуру поля, включая обратимые элементы и скалярные умножения.
LaTeX
$$ Field (HahnSeries Γ R) $$
Lean4
instance instField : Field (HahnSeries Γ R)
where
inv_zero := by simp [inv_def]
mul_inv_cancel x
x0 :=
by
have h :=
SummableFamily.one_sub_self_mul_hsum_powers
(unit_aux x (inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr x0)) _ (neg_add_cancel x.order))
rw [sub_sub_cancel] at h
rw [inv_def, ← mul_assoc, mul_comm x, h]
nnqsmul := (· • ·)
qsmul := (· • ·)
nnqsmul_def q x := by ext; simp [← single_zero_nnratCast, NNRat.smul_def]
qsmul_def q x := by ext; simp [← single_zero_ratCast, Rat.smul_def]
nnratCast_def q := by simp [← single_zero_nnratCast, ← single_zero_natCast, NNRat.cast_def]
ratCast_def q := by simp [← single_zero_ratCast, ← single_zero_intCast, ← single_zero_natCast, Rat.cast_def]
