coroot_eq_smul_coroot_iff — Mathlib

English

Under finiteness and no-zero-smul-divisors hypotheses, coroot i = t · coroot j iff root j = t · root i.

Русский

При конечности и отсутствии нулевых делителей в Smul, короот i = t · короот j тогда и только тогда, когда корень j = t · корень i.

LaTeX

$$$ P.coroot(i) = t \cdot P.coroot(j) \iff P.root(j) = t \cdot P.root(i) $$$

Lean4

@[simp]
theorem coroot_eq_smul_coroot_iff [Finite ι] [NoZeroSMulDivisors ℤ M] [NoZeroSMulDivisors ℤ N] {i j : ι} {t : R} :
    P.coroot i = t • P.coroot j ↔ P.root j = t • P.root i :=
  ⟨fun h ↦ (P.flip.smul_coroot_eq_of_root_eq_smul j i t h).symm, fun h ↦
    (P.smul_coroot_eq_of_root_eq_smul i j t h).symm⟩

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