inj_right — Mathlib

English

If φ is homogeneous of degree m and also homogeneous of degree n, and φ ≠ 0, then m = n.

Русский

Если φ однороден по степени m и по степени n, и φ ≠ 0, то m = n.

LaTeX

$$(IsHomogeneous(\phi, m) \land IsHomogeneous(\phi, n) \land \phi \neq 0) \Rightarrow m = n$$

Lean4

theorem inj_right (hm : IsHomogeneous φ m) (hn : IsHomogeneous φ n) (hφ : φ ≠ 0) : m = n :=
  by
  obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero hφ
  rw [← hm hd, ← hn hd]

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