dual_dual — Mathlib

English

A balance between duals and divisions: dual(J)/dual(I) = I/J; this expresses a cross-compatibility between taking duals and quotients.

Русский

Баланс дуалов и делений: dual(J)/dual(I) = I/J; это выражает совместимость операций дуализации и деления.

LaTeX

$$\frac{\mathrm{dual}_{A,K}(J)}{\mathrm{dual}_{A,K}(I)} = \frac{I}{J}$$

Lean4

@[simp]
theorem dual_dual : dual A K (dual A K I) = I :=
  by
  rw [dual_eq_mul_inv, dual_eq_mul_inv A K (I := I), mul_inv, inv_inv, ← mul_assoc, mul_inv_cancel₀, one_mul]
  rw [dual_ne_zero_iff]
  exact one_ne_zero

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