dualCopairing_eq — Mathlib

English

The symmetrized equivalence sends φ to its image evaluated at Quotient.mk x, i.e., (dualQuotEquivDualAnnihilator W).symm φ (Quotient.mk x) = φ x.

Русский

Симметричное эквивалентное отображение переводит φ в φ(x) на классе Quotient.mk x: (dualQuotEquivDualAnnihilator W).symm φ (Quotient.mk x) = φ x.

LaTeX

$$$(dualQuotEquivDualAnnihilator W).symm(\varphi)(\overline{x}) = \varphi(x)$$$

Lean4

theorem dualCopairing_eq (W : Submodule R M) : W.dualCopairing = (dualQuotEquivDualAnnihilator W).symm.toLinearMap :=
  rfl

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