Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-11 10:11 c9b80414

View on Github →

feat(linear_algebra/dual): more about dual_annihilator (#17313) Also gives dual_annihilator_sup_eq_inf_dual_annihilator a shorter name.

Estimated changes

Modified src/linear_algebra/bilinear_form.lean

Modified src/linear_algebra/dual.lean

added theorem module.eval_apply_eq_zero_iff

added theorem module.eval_apply_injective

added theorem module.forall_dual_apply_eq_zero_iff

added theorem submodule.dual_annihilator_anti

added theorem submodule.dual_annihilator_bot

added theorem submodule.dual_annihilator_comap_anti

added theorem submodule.dual_annihilator_comap_bot

added theorem submodule.dual_annihilator_sup_eq

deleted theorem submodule.dual_annihilator_sup_eq_inf_dual_annihilator

added theorem submodule.dual_annihilator_supr_eq

added theorem submodule.dual_annihilator_top

added theorem submodule.le_dual_annihilator_comap_dual_annihilator

added theorem submodule.le_dual_annihilator_dual_annihilator_comap

added theorem submodule.mem_dual_annihilator_comap

deleted theorem submodule.mem_dual_annihilator_comap_iff

added theorem submodule.sup_dual_annihilator_le_inf

added theorem submodule.supr_dual_annihilator_le_infi

added theorem subspace.dual_annihilator_comap_top

added theorem subspace.dual_annihilator_dual_annihilator_comap_eq