Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-18 05:31 017acaee

View on Github →

feat(linear_algebra/dual): adds dual annihilators (#6078)

Estimated changes

Modified src/linear_algebra/basic.lean

added def linear_map.dom_restrict'

added theorem linear_map.dom_restrict'_apply

Modified src/linear_algebra/dual.lean

added def submodule.dual_annihilator

added def submodule.dual_restrict

added theorem submodule.dual_restrict_apply

added theorem submodule.dual_restrict_ker_eq_dual_annihilator

added theorem submodule.mem_dual_annihilator

added theorem subspace.dual_equiv_dual_apply

added theorem subspace.dual_equiv_dual_def

added theorem subspace.dual_lift_injective

added theorem subspace.dual_lift_of_mem

added theorem subspace.dual_lift_of_subtype

added theorem subspace.dual_lift_right_inverse

added theorem subspace.dual_restrict_comp_dual_lift

added theorem subspace.dual_restrict_left_inverse

added theorem subspace.dual_restrict_surjective

Modified src/linear_algebra/finite_dimensional.lean