dualQuotEquivDualAnnihilator_apply

English

For W and φ in (M/W)^*, and x in M, the application of the inverse equivalence to φ evaluated at Quotient.mk x equals φ(x).

Русский

Для W и φ ∈ (M/W)^*, и x ∈ M, применение обратного соответствия к φ на Quotient.mk x равно φ(x).

LaTeX

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

Lean4

@[simp]
theorem dualQuotEquivDualAnnihilator_apply (W : Submodule R M) (φ : Module.Dual R (M ⧸ W)) (x : M) :
    dualQuotEquivDualAnnihilator W φ x = φ (Quotient.mk x) :=
  rfl

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