English
For rings R, IsLeftCancelMulZero in R[X] is equivalent to IsLeftCancelMulZero in R together with IsCancelAdd in R.
Русский
Для колец R, свойство IsLeftCancelMulZero в R[X] эквивалентно IsLeftCancelMulZero в R и IsCancelAdd в R.
LaTeX
$$$\operatorname{IsLeftCancelMulZero}(R[X]) \iff \operatorname{IsLeftCancelMulZero}(R) \land \operatorname{IsCancelAdd}(R)$$$
Lean4
theorem isLeftCancelMulZero_iff : IsLeftCancelMulZero R[X] ↔ IsLeftCancelMulZero R ∧ IsCancelAdd R
where
mp
h :=
.intro (C_injective.isLeftCancelMulZero _ C_0 fun _ _ ↦ C_mul) <|
have : IsLeftCancelAdd R :=
.mk fun a b c eq ↦ by
nontriviality R
let trinomial (r : R) : R[X] := a • X ^ 2 + r • X + C a
have ht r : (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a :=
by
simp only [trinomial, mul_add, add_mul, ← C_mul', C_1, one_mul, ← mul_assoc, X_mul_C, C_add]
noncomm_ring
simpa [trinomial] using
congr_arg (coeff · 1) <|
h.1 (a₁ := trinomial b) (a₂ := trinomial c) (X_add_C_ne_zero 1) <| by simp_rw [ht, eq]
AddCommMagma.IsLeftCancelAdd.toIsCancelAdd R
mpr := fun ⟨_, _⟩ ↦ inferInstance
