Defs

📁 Source: Mathlib/LinearAlgebra/Dual/Defs.lean

Statistics

Metric	Count
Definitions dualMap, dualMap, eval, instInhabited, transpose, IsReflexive, dualPairing, evalEquiv, mapEvalEquiv, dualAnnihilator, dualCoannihilator, dualRestrict	12
Theorems apply_one_mul_eq, dualMap_apply, dualMap_refl, dualMap_symm, dualMap_trans, dualCoannihilator_range_eq_ker_flip, dualMap_apply, dualMap_apply', dualMap_comp_dualMap, dualMap_def, dualMap_eq_lcomp, dualMap_id, dualMap_injective_of_surjective, ker_dualMap_eq_dualAnnihilator_range, ker_dualMap_eq_dualCoannihilator_range, range_dualMap_dual_eq_span_singleton, range_dualMap_le_dualAnnihilator_ker, eval_apply, eval_comp_comp_evalEquiv_eq, eval_naturality, instIsReflecive, transpose_apply, transpose_comp, bijective_dual_eval', of_split, to_isTorsionFree, apply_evalEquiv_symm_apply, bijective_dual_eval, dualMap_dualMap_eq_iff, dualMap_dualMap_eq_iff_of_injective, dualPairing_apply, equiv, erange_coe, evalEquiv_apply, evalEquiv_toLinearMap, mapEvalEquiv_apply, mapEvalEquiv_symm_apply, symm_dualMap_evalEquiv, instModuleIsReflexive, coe_dualAnnihilator_span, coe_dualCoannihilator_span, comap_dualAnnihilator, dualAnnihilator_anti, dualAnnihilator_bot, dualAnnihilator_dualCoannihilator_dualAnnihilator, dualAnnihilator_gc, dualAnnihilator_iSup_eq, dualAnnihilator_map_dualMap_le, dualAnnihilator_sup_eq, dualAnnihilator_top, dualCoannihilator_anti, dualCoannihilator_bot, dualCoannihilator_dualAnnihilator_dualCoannihilator, dualCoannihilator_iSup_eq, dualCoannihilator_sup_eq, dualRestrict_apply, dualRestrict_def, dualRestrict_ker_eq_dualAnnihilator, iSup_dualAnnihilator_le_iInf, le_dualAnnihilator_dualCoannihilator, le_dualAnnihilator_iff_le_dualCoannihilator, le_dualCoannihilator_dualAnnihilator, map_dualCoannihilator_le, mem_dualAnnihilator, mem_dualCoannihilator, sup_dualAnnihilator_le_inf	66
Total	78

Dual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_one_mul_eq 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe Module.Dual NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.instFunLike RingHom.id AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mul_one smul_eq_mul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass mul_comm

LinearEquiv

Definitions

Name	Category	Theorems
dualMap 📖	CompOp	11 math math: dualMap_trans, symm_flip, QuadraticForm.dualProdIsometry_invFun, Module.symm_dualMap_evalEquiv, dualMap_symm, QuadraticForm.dualProdIsometry_toFun, RootPairing.reflection_dualMap_eq_coreflection, dualMap_apply, dualMap_refl, trans_dualMap_symm_flip, SpecialLinearGroup.coe_dualMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dualMap_apply 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearEquiv RingHomInvPair.ids LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike dualMap	—	RingHomInvPair.ids smulCommClass_self
dualMap_refl 📖	mathematical	—	dualMap refl CommSemiring.toSemiring Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	ext smulCommClass_self RingHomInvPair.ids LinearMap.ext
dualMap_symm 📖	mathematical	—	symm Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomInvPair.ids dualMap	—	RingHomInvPair.ids smulCommClass_self
dualMap_trans 📖	mathematical	—	trans Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomCompTriple.ids RingHomInvPair.ids dualMap	—	RingHomInvPair.ids smulCommClass_self RingHomCompTriple.ids

LinearMap

Definitions

Name	Category	Theorems
dualMap 📖	CompOp	34 math math: Module.Dual.eval_comp_comp_evalEquiv_eq, Module.dualMap_dualMap_eq_iff, Submodule.dualAnnihilator_map_dualMap_le, RootPairing.Hom.weight_coweight_transpose, RootPairing.injOn_dualMap_subtype_span_root_coroot, dualMap_surjective_of_injective, SeparatingDual.dualMap_surjective_iff, dualMap_id, range_dualMap_eq_dualAnnihilator_ker, range_dualMap_dual_eq_span_singleton, Submodule.dualRestrict_def, dualMap_injective_of_surjective, dualMap_injective_iff, dualMap_apply', dualMap_bijective_iff, det_dualMap, RootPairing.Hom.weight_coweight_transpose_apply, range_dualMap_eq_dualAnnihilator_ker_of_surjective, Module.injOn_dualMap_subtype_span_range_range, ker_dualMap_eq_dualCoannihilator_range, finrank_range_dualMap_eq_finrank_range, dualMap_apply, dualMap_surjective_iff, dualMap_def, RootPairing.toPerfPair_conj_reflection, Submodule.range_dualMap_mkQ_eq, Module.dualMap_dualMap_eq_iff_of_injective, range_dualMap_le_dualAnnihilator_ker, RootPairing.toPerfPair_flip_conj_coreflection, Module.Dual.eval_naturality, dualMap_comp_dualMap, dualMap_eq_lcomp, Module.Dual.eq_of_preReflection_mapsTo', ker_dualMap_eq_dualAnnihilator_range

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dualCoannihilator_range_eq_ker_flip 📖	mathematical	—	Submodule.dualCoannihilator range LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomSurjective.ids ker SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero flip	—	smulCommClass_self Submodule.ext RingHomSurjective.ids SMulCommClass.symm ext_iff
dualMap_apply 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction dualMap	—	smulCommClass_self
dualMap_apply' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike dualMap comp RingHomCompTriple.ids	—	smulCommClass_self
dualMap_comp_dualMap 📖	mathematical	—	comp Module.Dual CommSemiring.toSemiring addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomCompTriple.ids dualMap	—	smulCommClass_self RingHomCompTriple.ids
dualMap_def 📖	mathematical	—	dualMap DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instFunLike Module.Dual.transpose	—	smulCommClass_self
dualMap_eq_lcomp 📖	mathematical	—	dualMap lcomp CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self
dualMap_id 📖	mathematical	—	dualMap id CommSemiring.toSemiring Module.Dual addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	ext smulCommClass_self
dualMap_injective_of_surjective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike	Module.Dual addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction dualMap	—	smulCommClass_self ext
ker_dualMap_eq_dualAnnihilator_range 📖	mathematical	—	ker Module.Dual CommSemiring.toSemiring addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction dualMap Submodule.dualAnnihilator range RingHomSurjective.ids	—	Submodule.ext smulCommClass_self RingHomSurjective.ids
ker_dualMap_eq_dualCoannihilator_range 📖	mathematical	—	ker Module.Dual CommSemiring.toSemiring addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction dualMap Submodule.dualCoannihilator range RingHomSurjective.ids comp RingHomCompTriple.ids Module.Dual.eval	—	Submodule.ext smulCommClass_self RingHomSurjective.ids RingHomCompTriple.ids ext_iff
range_dualMap_dual_eq_span_singleton 📖	mathematical	—	range Module.Dual CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule addCommMonoid RingHom.id module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomSurjective.ids dualMap Submodule.span Set Set.instSingletonSet	—	Submodule.ext smulCommClass_self RingHomSurjective.ids Submodule.mem_span_singleton ext Dual.apply_one_mul_eq RingHomCompTriple.ids map_smul SemilinearMapClass.toMulActionSemiHomClass semilinearMapClass
range_dualMap_le_dualAnnihilator_ker 📖	mathematical	—	Submodule Module.Dual CommSemiring.toSemiring addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder range RingHomSurjective.ids dualMap Submodule.dualAnnihilator ker	—	smulCommClass_self RingHomSurjective.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass

Module

Definitions

Name	Category	Theorems
IsReflexive 📖	CompData	10 math math: LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive, ULift.instModuleIsReflexive, Dual.instIsReflecive, IsReflexive.of_split, instIsReflexiveOfFiniteOfProjective, Prod.instModuleIsReflexive, equiv, IsReflexive.of_finite_of_free, IsReflexive.of_isPerfPair, MulOpposite.instModuleIsReflexive
dualPairing 📖	CompOp	2 math math: LinearMap.dualPairing_nondegenerate, dualPairing_apply
evalEquiv 📖	CompOp	6 math math: Dual.eval_comp_comp_evalEquiv_eq, LinearEquiv.symm_flip, symm_dualMap_evalEquiv, evalEquiv_apply, apply_evalEquiv_symm_apply, evalEquiv_toLinearMap
mapEvalEquiv 📖	CompOp	3 math math: Subspace.dualAnnihilator_dualAnnihilator_eq, mapEvalEquiv_apply, mapEvalEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_evalEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearEquiv RingHomInvPair.ids LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm evalEquiv	—	smulCommClass_self RingHomInvPair.ids LinearEquiv.apply_symm_apply evalEquiv_apply Dual.eval_apply
bijective_dual_eval 📖	mathematical	—	Function.Bijective Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction DFunLike.coe LinearMap LinearMap.instFunLike Dual.eval	—	IsReflexive.bijective_dual_eval'
dualMap_dualMap_eq_iff 📖	mathematical	—	LinearMap.dualMap Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction	—	dualMap_dualMap_eq_iff_of_injective Function.Bijective.injective smulCommClass_self bijective_dual_eval
dualMap_dualMap_eq_iff_of_injective 📖	mathematical	Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction DFunLike.coe LinearMap LinearMap.instFunLike Dual.eval	LinearMap.dualMap	—	smulCommClass_self RingHomCompTriple.ids RingHomInvPair.ids LinearEquiv.eq_comp_toLinearMap_iff LinearMap.cancel_left
dualPairing_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike Dual LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction dualPairing	—	smulCommClass_self
equiv 📖	mathematical	—	IsReflexive	—	RingHomInvPair.ids smulCommClass_self RingHomCompTriple.ids LinearMap.ext DFunLike.congr_arg LinearEquiv.apply_symm_apply Function.Bijective.comp bijective_dual_eval LinearEquiv.bijective
erange_coe 📖	mathematical	—	LinearMap.range Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction RingHomSurjective.ids Dual.eval Top.top Submodule Submodule.instTop	—	smulCommClass_self RingHomSurjective.ids LinearMap.range_eq_top bijective_dual_eval
evalEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike evalEquiv LinearMap LinearMap.instFunLike Dual.eval	—	smulCommClass_self RingHomInvPair.ids
evalEquiv_toLinearMap 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction evalEquiv Dual.eval	—	smulCommClass_self RingHomInvPair.ids
mapEvalEquiv_apply 📖	mathematical	—	DFunLike.coe OrderIso Submodule CommSemiring.toSemiring Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder instFunLikeOrderIso mapEvalEquiv Submodule.map RingHomSurjective.ids Dual.eval	—	smulCommClass_self
mapEvalEquiv_symm_apply 📖	mathematical	—	DFunLike.coe OrderIso Submodule Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder instFunLikeOrderIso OrderIso.symm mapEvalEquiv Submodule.comap Dual.eval	—	smulCommClass_self
symm_dualMap_evalEquiv 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction LinearEquiv.dualMap LinearEquiv.symm evalEquiv Dual.eval	—	LinearMap.ext smulCommClass_self RingHomInvPair.ids apply_evalEquiv_symm_apply

Module.Dual

Definitions

Name	Category	Theorems
eval 📖	CompOp	32 math math: Subspace.dualAnnihilator_dualAnnihilator_eq_map, Submodule.map_dualCoannihilator_le, eval_comp_comp_evalEquiv_eq, Module.eval_apply_injective, Module.mapEvalEquiv_apply, Module.comap_eval_surjective, eval_apply, Module.preReflection_preReflection, Submodule.comap_dualAnnihilator, transpose_dualTensorHom, Module.Basis.eval_range, Module.IsReflexive.bijective_dual_eval', Module.symm_dualMap_evalEquiv, Module.eval_apply_eq_zero_iff, Module.Basis.toDual_toDual, Module.eval_ker, Module.Basis.eval_injective, Module.evalEquiv_apply, LinearMap.ker_dualMap_eq_dualCoannihilator_range, Module.bijective_dual_eval, Subspace.map_le_dualAnnihilator_dualAnnihilator, eval_naturality, Module.map_eval_injective, Module.evalEquiv_toLinearMap, Subspace.map_dualCoannihilator, LinearEquiv.trans_dualMap_symm_flip, Module.Basis.eval_ker, Subspace.comap_dualAnnihilator_dualAnnihilator, Module.erange_coe, Module.mapEvalEquiv_symm_apply, LinearMap.IsPerfPair.dualEval, LinearMap.separatingLeft_dualProd
instInhabited 📖	CompOp	—
transpose 📖	CompOp	9 math math: LinearMap.toMatrix_transpose, LinearMap.trace_transpose', transpose_apply, transpose_comp, transpose_dualTensorHom, LinearMap.trace_transpose, LinearMap.dualMap_def, Matrix.toLin_transpose, Representation.dual_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eval_apply 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike LinearMap eval	—	smulCommClass_self
eval_comp_comp_evalEquiv_eq 📖	mathematical	—	LinearMap.comp Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomCompTriple.ids eval LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm Module.evalEquiv LinearMap.dualMap	—	smulCommClass_self RingHomCompTriple.ids RingHomInvPair.ids LinearMap.comp_assoc LinearEquiv.comp_toLinearMap_symm_eq Module.evalEquiv_toLinearMap eval_naturality
eval_naturality 📖	mathematical	—	LinearMap.comp Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomCompTriple.ids LinearMap.dualMap eval	—	smulCommClass_self RingHomCompTriple.ids
instIsReflecive 📖	mathematical	—	Module.IsReflexive Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	smulCommClass_self RingHomInvPair.ids LinearEquiv.bijective
transpose_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero transpose LinearMap.comp RingHomCompTriple.ids	—	smulCommClass_self LinearMap.instSMulCommClass
transpose_comp 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike transpose LinearMap.comp RingHomCompTriple.ids	—	smulCommClass_self LinearMap.instSMulCommClass RingHomCompTriple.ids

Module.IsReflexive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_dual_eval' 📖	mathematical	—	Function.Bijective Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction DFunLike.coe LinearMap LinearMap.instFunLike Module.Dual.eval	—	—
of_split 📖	mathematical	LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.id	Module.IsReflexive	—	RingHomCompTriple.ids smulCommClass_self Function.Injective.of_comp Module.bijective_dual_eval LinearMap.injective_of_comp_eq_id RingHomInvPair.ids Function.Surjective.of_comp LinearMap.surjective_of_comp_eq_id
to_isTorsionFree 📖	mathematical	—	Module.IsTorsionFree CommSemiring.toSemiring	—	Function.Bijective.injective smulCommClass_self Module.bijective_dual_eval LinearMap.ext map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass IsRegular.left

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instModuleIsReflexive 📖	mathematical	—	Module.IsReflexive MulOpposite instAddCommMonoid instModule CommSemiring.toSemiring	—	Module.equiv

Submodule

Definitions

Name	Category	Theorems
dualAnnihilator 📖	CompOp	68 math math: Subspace.dualAnnihilator_dualAnnihilator_eq_map, dualAnnihilator_dualCoannihilator_dualAnnihilator, map_dualCoannihilator_le, RootPairing.rootSpan_dualAnnihilator_le_ker_rootForm, dualQuotEquivDualAnnihilator_apply, dualPairing_apply, Subspace.dualCoannihilator_dualAnnihilator_eq, Subspace.dualAnnihilator_dualAnnihilator_eq, le_dualAnnihilator_dualCoannihilator, dualAnnihilator_map_dualMap_le, dualCopairing_eq, mem_dualAnnihilator, dualAnnihilator_eq_top_iff, Subspace.finrank_dualCoannihilator_eq, dualAnnihilator_anti, Subspace.dualPairing_nondegenerate, dualCoannihilator_dualAnnihilator_dualCoannihilator, dualRestrict_ker_eq_dualAnnihilator, LinearMap.IsPerfectCompl.isCompl_right, comap_dualAnnihilator, iSup_dualAnnihilator_le_iInf, LinearMap.range_dualMap_eq_dualAnnihilator_ker, dualCoannihilator_map_linearEquiv_flip, RootPairing.corootSpan_dualAnnihilator_map_eq, dualAnnihilator_sup_eq, dualCopairing_apply, Subspace.quotAnnihilatorEquiv_apply, LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_surjective, Subspace.dualAnnihilator_inj, dualAnnihilator_gc, RootPairing.ker_rootForm_eq_dualAnnihilator, sup_dualAnnihilator_le_inf, Subspace.dualAnnihilator_iInf_eq, coe_dualAnnihilator_span, Subspace.dualCopairing_nondegenerate, dualAnnihilator_top, Subspace.map_le_dualAnnihilator_dualAnnihilator, RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root', LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective, range_dualMap_mkQ_eq, LinearMap.range_dualMap_le_dualAnnihilator_ker, finite_dualAnnihilator_iff, Subspace.dualAnnihilator_le_dualAnnihilator_iff, le_dualAnnihilator_iff_le_dualCoannihilator, dualAnnihilator_bot, RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm, RootPairing.rootSpan_dualAnnihilator_map_eq, dualAnnihilator_map_linearEquiv_flip_symm, dualAnnihilator_iSup_eq, dualAnnihilator_eq_bot_iff, dualAnnihilator_eq_bot_iff', map_dualCoannihilator_linearEquiv_flip, dualQuotEquivDualAnnihilator_symm_apply_mk, Subspace.map_dualCoannihilator, RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot', RootPairing.invtSubmodule_reflection_of_invtSubmodule_coreflection, LinearMap.ker_dualMap_eq_dualAnnihilator_range, RootPairing.ker_corootForm_eq_dualAnnihilator, Subspace.dualAnnihilator_inf_eq, Subspace.dualAnnihilator_dualCoannihilator_eq, LinearMap.IsPerfectCompl.isCompl_left, map_dualAnnihilator_linearEquiv_flip_symm, Subspace.isCompl_dualAnnihilator, Subspace.comap_dualAnnihilator_dualAnnihilator, le_dualCoannihilator_dualAnnihilator, Subspace.finrank_add_finrank_dualAnnihilator_eq, Subspace.dualPairing_eq, LinearMap.dualAnnihilator_ker_eq_range_flip
dualCoannihilator 📖	CompOp	38 math math: dualAnnihilator_dualCoannihilator_dualAnnihilator, map_dualCoannihilator_le, quotDualCoannihilatorToDual_apply, Subspace.dualCoannihilator_dualAnnihilator_eq, le_dualAnnihilator_dualCoannihilator, quotDualCoannihilatorToDual_nondegenerate, coe_dualCoannihilator_span, Subspace.finrank_dualCoannihilator_eq, Subspace.finiteDimensional_quot_dualCoannihilator_iff, dualCoannihilator_dualAnnihilator_dualCoannihilator, dualCoannihilator_iSup_eq, comap_dualAnnihilator, dualCoannihilator_map_linearEquiv_flip, dualCoannihilator_anti, RootPairing.corootSpan_dualAnnihilator_map_eq, dualCoannihilator_bot, dualCoannihilator_top, Subspace.flip_quotDualCoannihilatorToDual_bijective, dualCoannihilator_sup_eq, RootPairing.iInf_ker_root'_eq, mem_dualCoannihilator, RootPairing.iInf_ker_coroot'_eq, Subspace.finrank_add_finrank_dualCoannihilator_eq, dualAnnihilator_gc, quotDualCoannihilatorToDual_injective, LinearMap.ker_dualMap_eq_dualCoannihilator_range, le_dualAnnihilator_iff_le_dualCoannihilator, RootPairing.rootSpan_dualAnnihilator_map_eq, dualAnnihilator_map_linearEquiv_flip_symm, LinearMap.BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal, map_dualCoannihilator_linearEquiv_flip, Subspace.map_dualCoannihilator, LinearMap.dualCoannihilator_range_eq_ker_flip, Subspace.quotDualCoannihilatorToDual_bijective, Subspace.dualAnnihilator_dualCoannihilator_eq, map_dualAnnihilator_linearEquiv_flip_symm, le_dualCoannihilator_dualAnnihilator, flip_quotDualCoannihilatorToDual_injective
dualRestrict 📖	CompOp	8 math math: Subspace.dualRestrict_comp_dualLift, dualRestrict_ker_eq_dualAnnihilator, dualRestrict_def, Subspace.dualRestrict_leftInverse, Subspace.quotAnnihilatorEquiv_apply, Subspace.dualRestrict_surjective, Subspace.dualLift_rightInverse, dualRestrict_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_dualAnnihilator_span 📖	mathematical	—	SetLike.coe Submodule Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction setLike dualAnnihilator span setOf LinearMap Set Set.instHasSubset LinearMap.ker	—	Set.ext smulCommClass_self span_le
coe_dualCoannihilator_span 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring setLike dualCoannihilator span Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction setOf	—	Set.ext smulCommClass_self span_le
comap_dualAnnihilator 📖	mathematical	—	comap Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Module.Dual.eval dualAnnihilator dualCoannihilator	—	smulCommClass_self
dualAnnihilator_anti 📖	mathematical	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder	Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction dualAnnihilator	—	GaloisConnection.monotone_l smulCommClass_self dualAnnihilator_gc
dualAnnihilator_bot 📖	mathematical	—	dualAnnihilator Bot.bot Submodule CommSemiring.toSemiring instBot Top.top Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instTop	—	GaloisConnection.l_bot smulCommClass_self dualAnnihilator_gc
dualAnnihilator_dualCoannihilator_dualAnnihilator 📖	mathematical	—	dualAnnihilator dualCoannihilator	—	GaloisConnection.l_u_l_eq_l smulCommClass_self dualAnnihilator_gc
dualAnnihilator_gc 📖	mathematical	—	GaloisConnection Submodule CommSemiring.toSemiring OrderDual Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction PartialOrder.toPreorder instPartialOrder OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual dualAnnihilator dualCoannihilator OrderDual.ofDual	—	smulCommClass_self instIsConcreteLE
dualAnnihilator_iSup_eq 📖	mathematical	—	dualAnnihilator iSup Submodule CommSemiring.toSemiring ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice iInf Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instInfSet	—	GaloisConnection.l_iSup smulCommClass_self dualAnnihilator_gc
dualAnnihilator_map_dualMap_le 📖	mathematical	—	Submodule Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder map RingHomSurjective.ids LinearMap.dualMap dualAnnihilator comap	—	smulCommClass_self RingHomSurjective.ids
dualAnnihilator_sup_eq 📖	mathematical	—	dualAnnihilator Submodule CommSemiring.toSemiring SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instMin	—	GaloisConnection.l_sup smulCommClass_self dualAnnihilator_gc
dualAnnihilator_top 📖	mathematical	—	dualAnnihilator Top.top Submodule CommSemiring.toSemiring instTop Bot.bot Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instBot	—	smulCommClass_self instIsConcreteLE
dualCoannihilator_anti 📖	mathematical	Submodule Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder	dualCoannihilator	—	smulCommClass_self GaloisConnection.monotone_u dualAnnihilator_gc
dualCoannihilator_bot 📖	mathematical	—	dualCoannihilator Bot.bot Submodule Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instBot Top.top instTop	—	GaloisConnection.u_top smulCommClass_self dualAnnihilator_gc
dualCoannihilator_dualAnnihilator_dualCoannihilator 📖	mathematical	—	dualCoannihilator dualAnnihilator	—	smulCommClass_self GaloisConnection.u_l_u_eq_u dualAnnihilator_gc
dualCoannihilator_iSup_eq 📖	mathematical	—	dualCoannihilator iSup Submodule Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice iInf instInfSet	—	smulCommClass_self GaloisConnection.u_iInf dualAnnihilator_gc
dualCoannihilator_sup_eq 📖	mathematical	—	dualCoannihilator Submodule Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice instMin	—	smulCommClass_self GaloisConnection.u_inf dualAnnihilator_gc
dualRestrict_apply 📖	mathematical	—	DFunLike.coe Module.Dual Submodule CommSemiring.toSemiring SetLike.instMembership setLike addCommMonoid module LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction dualRestrict	—	smulCommClass_self
dualRestrict_def 📖	mathematical	—	dualRestrict LinearMap.dualMap Submodule CommSemiring.toSemiring SetLike.instMembership setLike addCommMonoid module subtype	—	smulCommClass_self
dualRestrict_ker_eq_dualAnnihilator 📖	mathematical	—	LinearMap.ker Module.Dual CommSemiring.toSemiring Submodule SetLike.instMembership setLike addCommMonoid module LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction dualRestrict dualAnnihilator	—	smulCommClass_self
iSup_dualAnnihilator_le_iInf 📖	mathematical	—	Submodule Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice dualAnnihilator iInf instInfSet	—	smulCommClass_self le_dualAnnihilator_iff_le_dualCoannihilator dualCoannihilator_iSup_eq iInf_mono le_dualAnnihilator_dualCoannihilator
le_dualAnnihilator_dualCoannihilator 📖	mathematical	—	Submodule CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder dualCoannihilator dualAnnihilator	—	GaloisConnection.le_u_l smulCommClass_self dualAnnihilator_gc
le_dualAnnihilator_iff_le_dualCoannihilator 📖	mathematical	—	Submodule Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder dualAnnihilator dualCoannihilator	—	smulCommClass_self GaloisConnection.le_iff_le dualAnnihilator_gc
le_dualCoannihilator_dualAnnihilator 📖	mathematical	—	Submodule Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder dualAnnihilator dualCoannihilator	—	smulCommClass_self GaloisConnection.l_u_le dualAnnihilator_gc
map_dualCoannihilator_le 📖	mathematical	—	Submodule Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder map RingHomSurjective.ids Module.Dual.eval dualCoannihilator dualAnnihilator	—	smulCommClass_self RingHomSurjective.ids map_le_iff_le_comap Eq.le comap_dualAnnihilator
mem_dualAnnihilator 📖	mathematical	—	Module.Dual CommSemiring.toSemiring Submodule LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.instMembership setLike dualAnnihilator DFunLike.coe LinearMap.instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	smulCommClass_self
mem_dualCoannihilator 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership setLike dualCoannihilator DFunLike.coe Module.Dual LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	smulCommClass_self
sup_dualAnnihilator_le_inf 📖	mathematical	—	Submodule Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice dualAnnihilator instMin	—	smulCommClass_self le_dualAnnihilator_iff_le_dualCoannihilator dualCoannihilator_sup_eq inf_le_inf le_dualAnnihilator_dualCoannihilator

---

← Back to Index