dual_eq_mul_inv — Mathlib

English

The dual of I equals the product of the dual of 1 with the inverse of I: dual(I) = dual(1) · I^{-1}.

Русский

Двойственная к I равна произведению двойственной единицы на обратную к I: dual(I) = dual(1) · I^{-1}.

LaTeX

$$\mathrm{dual}_{A,K}(I) = \mathrm{dual}_{A,K}(1) \cdot I^{-1}$$

Lean4

theorem dual_eq_mul_inv : dual A K I = dual A K 1 * I⁻¹ :=
  by
  by_cases hI : I = 0; · simp [hI]
  apply le_antisymm
  · suffices dual A K I * I ≤ dual A K 1 by convert mul_right_mono I⁻¹ this using 1;
      simp only [mul_inv_cancel₀ hI, mul_one, mul_assoc]
    rw [← le_dual_iff A K hI]
  rw [le_dual_iff A K hI, mul_assoc, inv_mul_cancel₀ hI, mul_one]

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