finite_dualAnnihilator_iff — Mathlib

English

If M/W is finite and free, then the dual annihilator W.dualAnnihilator is finite, and conversely.

Русский

Если M/W конечномерно свободно, то W.dualAnnihilator конечно; обратно — если W.dualAnnihilator конечно, то M/W конечно.

LaTeX

$$Module.Finite R W.dualAnnihilator ↔ Module.Finite R (M ⧸ W)$$

Lean4

theorem finite_dualAnnihilator_iff {W : Submodule R M} [Free R (M ⧸ W)] :
    Module.Finite R W.dualAnnihilator ↔ Module.Finite R (M ⧸ W) :=
  (Finite.equiv_iff W.dualQuotEquivDualAnnihilator.symm).trans (finite_dual_iff R)

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