dualCoannihilator_range_eq_ker_flip

English

For B: M →ₗ[R] M' →ₗ[R] R, the dual coannihilator of range B equals the kernel of B.flip.

Русский

Для B: M → M' → R дуальный коаннигиллятор образа B равен ядру B.flip.

LaTeX

$$$ (\\mathrm{range} \\, B).dualCoannihilator = \\ker (B.flip) $$$

Lean4

@[simp]
theorem dualCoannihilator_range_eq_ker_flip (B : M →ₗ[R] M' →ₗ[R] R) :
    (range B).dualCoannihilator = LinearMap.ker B.flip := by ext x; simp [LinearMap.ext_iff (f := B.flip x)]

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