natDegree_mul_C_eq_of_mul_eq_one — Mathlib

English

natDegree_mul_C_eq_of_mul_eq_one: (p · C a).natDegree = p.natDegree if a is invertible with inverse ai.

Русский

natDegree(p · C a) = natDegree(p) при существовании обратного a.

LaTeX

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

Lean4

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

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