English
In the dual-number ring K[ε], for any a,b there exists c such that either a c = b or b c = a.
Русский
В кольце двойственных чисел K[ε] для любых a,b существует c, такой что либо a c = b, либо b c = a.
LaTeX
$$$\exists c\in K[\varepsilon],\; a c = b \;\lor\; b c = a$$$
Lean4
theorem exists_mul_left_or_mul_right [DivisionRing K] (a b : K[ε]) : ∃ c, a * c = b ∨ b * c = a :=
by
rcases isUnit_or_isNilpotent a with ha | ha
· lift a to K[ε]ˣ using ha
exact ⟨a⁻¹ * b, by simp⟩
rcases isUnit_or_isNilpotent b with hb | hb
· lift b to K[ε]ˣ using hb
exact ⟨b⁻¹ * a, by simp⟩
rw [isNilpotent_iff_eps_dvd] at ha hb
obtain ⟨x, rfl⟩ := ha
obtain ⟨y, rfl⟩ := hb
suffices ∃ c, fst x * fst c = fst y ∨ fst y * fst c = fst x by simpa [TrivSqZeroExt.ext_iff] using this
rcases eq_or_ne (fst x) 0 with hx | hx
· refine ⟨ε, Or.inr ?_⟩
simp [hx]
refine ⟨inl ((fst x)⁻¹ * fst y), ?_⟩
simp [← mul_assoc, mul_inv_cancel₀ hx]
