Commit 2023-05-21 22:16 0adac462

View on Github →

feat: port LinearAlgebra.Dual (#3659)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Dual.lean

added theorem Basis.coe_dualBasis

added theorem Basis.coe_toDual_self

added def Basis.dualBasis

added theorem Basis.dualBasis_apply

added theorem Basis.dualBasis_apply_self

added theorem Basis.dualBasis_equivFun

added theorem Basis.dualBasis_repr

added theorem Basis.dual_rank_eq

added def Basis.evalEquiv

added theorem Basis.evalEquiv_toLinearMap

added theorem Basis.eval_ker

added theorem Basis.eval_range

added theorem Basis.sum_dual_apply_smul_coord

added def Basis.toDual

added def Basis.toDualEquiv

added theorem Basis.toDualEquiv_apply

added def Basis.toDualFlip

added theorem Basis.toDualFlip_apply

added theorem Basis.toDual_apply

added theorem Basis.toDual_apply_left

added theorem Basis.toDual_apply_right

added theorem Basis.toDual_eq_equivFun

added theorem Basis.toDual_eq_repr

added theorem Basis.toDual_inj

added theorem Basis.toDual_ker

added theorem Basis.toDual_range

added theorem Basis.toDual_toDual

added theorem Basis.toDual_total_left

added theorem Basis.toDual_total_right

added theorem Basis.total_coord

added theorem Basis.total_dualBasis

added def LinearEquiv.dualMap

added theorem LinearEquiv.dualMap_apply

added theorem LinearEquiv.dualMap_refl

added theorem LinearEquiv.dualMap_symm

added theorem LinearEquiv.dualMap_trans

added def LinearMap.dualMap

added theorem LinearMap.dualMap_apply'

added theorem LinearMap.dualMap_apply

added theorem LinearMap.dualMap_bijective_iff

added theorem LinearMap.dualMap_comp_dualMap

added theorem LinearMap.dualMap_def

added theorem LinearMap.dualMap_id

added theorem LinearMap.dualMap_injective_iff

added theorem LinearMap.dualMap_injective_of_surjective

added theorem LinearMap.dualMap_surjective_iff

added theorem LinearMap.dualMap_surjective_of_injective

added theorem LinearMap.dualPairing_nondegenerate

added theorem LinearMap.finrank_range_dualMap_eq_finrank_range

added theorem LinearMap.ker_dualMap_eq_dualAnnihilator_range

added theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker

added theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective

added theorem LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_surjective

added theorem LinearMap.range_dualMap_le_dualAnnihilator_ker

added def Module.Dual.eval

added theorem Module.Dual.eval_apply

added def Module.Dual.transpose

added theorem Module.Dual.transpose_apply

added theorem Module.Dual.transpose_comp

added def Module.Dual

added def Module.DualBases.basis

added theorem Module.DualBases.coe_basis

added theorem Module.DualBases.coe_dualBasis

added def Module.DualBases.coeffs

added theorem Module.DualBases.coeffs_apply

added theorem Module.DualBases.coeffs_lc

added theorem Module.DualBases.dual_lc

added def Module.DualBases.lc

added theorem Module.DualBases.lc_coeffs

added theorem Module.DualBases.lc_def

added theorem Module.DualBases.mem_of_mem_span

added structure Module.DualBases

added theorem Module.comap_eval_surjective

added def Module.dualPairing

added theorem Module.dualPairing_apply

added def Module.dualProdDualEquivDual

added theorem Module.dualProdDualEquivDual_apply

added theorem Module.dual_rank_eq

added theorem Module.erange_coe

added def Module.evalEquiv

added theorem Module.evalEquiv_toLinearMap

added theorem Module.eval_apply_eq_zero_iff

added theorem Module.eval_apply_injective

added theorem Module.eval_ker

added theorem Module.forall_dual_apply_eq_zero_iff

added def Module.mapEvalEquiv

added theorem Module.mapEvalEquiv_apply

added theorem Module.mapEvalEquiv_symm_apply

added theorem Module.map_eval_injective

added def Submodule.dualAnnihilator

added theorem Submodule.dualAnnihilator_anti

added theorem Submodule.dualAnnihilator_bot

added theorem Submodule.dualAnnihilator_dualCoannihilator_dualAnnihilator

added theorem Submodule.dualAnnihilator_gc

added theorem Submodule.dualAnnihilator_iSup_eq

added theorem Submodule.dualAnnihilator_sup_eq

added theorem Submodule.dualAnnihilator_top

added def Submodule.dualCoannihilator

added theorem Submodule.dualCoannihilator_anti

added theorem Submodule.dualCoannihilator_bot

added theorem Submodule.dualCoannihilator_dualAnnihilator_dualCoannihilator

added theorem Submodule.dualCoannihilator_iSup_eq

added theorem Submodule.dualCoannihilator_sup_eq

added def Submodule.dualCopairing

added theorem Submodule.dualCopairing_apply

added theorem Submodule.dualCopairing_eq

added def Submodule.dualPairing

added theorem Submodule.dualPairing_apply

added def Submodule.dualQuotEquivDualAnnihilator

added theorem Submodule.dualQuotEquivDualAnnihilator_apply

added theorem Submodule.dualQuotEquivDualAnnihilator_symm_apply_mk

added def Submodule.dualRestrict

added theorem Submodule.dualRestrict_apply

added theorem Submodule.dualRestrict_def

added theorem Submodule.dualRestrict_ker_eq_dualAnnihilator

added theorem Submodule.iSup_dualAnnihilator_le_iInf

added theorem Submodule.le_dualAnnihilator_dualCoannihilator

added theorem Submodule.le_dualAnnihilator_iff_le_dualCoannihilator

added theorem Submodule.le_dualCoannihilator_dualAnnihilator

added theorem Submodule.mem_dualAnnihilator

added theorem Submodule.mem_dualCoannihilator

added theorem Submodule.range_dualMap_mkQ_eq

added theorem Submodule.sup_dualAnnihilator_le_inf

added def Subspace.dualAnnihilatorGci

added theorem Subspace.dualAnnihilator_dualAnnihilator_eq

added theorem Subspace.dualAnnihilator_dualCoannihilator_eq

added theorem Subspace.dualAnnihilator_iInf_eq

added theorem Subspace.dualAnnihilator_inf_eq

added theorem Subspace.dualAnnihilator_inj

added theorem Subspace.dualAnnihilator_le_dualAnnihilator_iff

added theorem Subspace.dualCoannihilator_top

added theorem Subspace.dualCopairing_nondegenerate

added theorem Subspace.dualEquivDual_apply

added theorem Subspace.dualEquivDual_def

added theorem Subspace.dualLift_injective

added theorem Subspace.dualLift_of_mem

added theorem Subspace.dualLift_of_subtype

added theorem Subspace.dualLift_rightInverse

added theorem Subspace.dualPairing_eq

added theorem Subspace.dualPairing_nondegenerate

added def Subspace.dualQuotDistrib

added theorem Subspace.dualRestrict_comp_dualLift

added theorem Subspace.dualRestrict_leftInverse

added theorem Subspace.dualRestrict_surjective

added theorem Subspace.dual_finrank_eq

added theorem Subspace.finrank_add_finrank_dualCoannihilator_eq

added theorem Subspace.finrank_dualCoannihilator_eq

added theorem Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff

added theorem Subspace.isCompl_dualAnnihilator

added theorem Subspace.quotAnnihilatorEquiv_apply

added def TensorProduct.dualDistrib

added theorem TensorProduct.dualDistribInvOfBasis_apply

added theorem TensorProduct.dualDistrib_apply

added theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse

added theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse

added def evalUseFiniteInstance