natDegree_C_mul_eq_of_mul_eq_one — Mathlib

English

natDegree_mul_C_eq_of_mul_eq_one: If ai · a = 1, then natDegree(C a · p) = natDegree(p).

Русский

Если ai · a = 1, то natDegree(C a · p) = natDegree(p).

LaTeX

$$$ai \\cdot a = 1 \\Rightarrow \\operatorname{natDegree}(\\,C a \\cdot p\\,) = \\operatorname{natDegree}(p)$$$

Lean4

theorem natDegree_C_mul_eq_of_mul_eq_one {ai : R} (au : ai * a = 1) : (C a * p).natDegree = p.natDegree :=
  le_antisymm (natDegree_C_mul_le a p)
    (calc
      p.natDegree = (1 * p).natDegree := by nth_rw 1 [← one_mul p]
      _ = (C ai * (C a * p)).natDegree := by rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]
      _ ≤ (C a * p).natDegree := natDegree_C_mul_le ai (C a * p))

Похожие утверждения