dualCopairing_apply — Mathlib

English

For any φ in W.dualAnnihilator and any x in M, the evaluation of the copairing on the coset x+W is just φ(x).

Русский

Для любого φ ∈ W.dualAnnihilator и любого x ∈ M значение копэрирования на классe x+W равно φ(x).

LaTeX

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

Lean4

@[simp]
theorem dualCopairing_apply {W : Submodule R M} (φ : W.dualAnnihilator) (x : M) :
    W.dualCopairing φ (Quotient.mk x) = φ x :=
  rfl

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