Lemmas

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

Statistics

Metric	Count
Definitions `dualProdDualEquivDual`, `dualCopairing`, `dualPairing`, `dualQuotEquivDualAnnihilator`, `instFunLikeSubtypeDualMemDualAnnihilator`, `quotDualCoannihilatorToDual`, `dualAnnihilatorGci`, `dualEquivDual`, `dualLift`, `dualQuotDistrib`, `orderIsoFiniteCodimDim`, `orderIsoFiniteDimensional`, `quotAnnihilatorEquiv`, `quotDualEquivAnnihilator`, `quotEquivAnnihilator`, `dualDistrib`, `dualDistrib`, `dualDistribEquiv`, `dualDistribEquivOfBasis`, `dualDistribInvOfBasis`	20
Theorems `linearEquiv_dual_iff_finiteDimensional`, `mem_span_of_iInf_ker_le_ker`, `dualAnnihilator_ker_eq_range_flip`, `dualMap_bijective_iff`, `dualMap_injective_iff`, `dualMap_surjective_iff`, `dualMap_surjective_of_injective`, `dualPairing_nondegenerate`, `finrank_range_dualMap_eq_finrank_range`, `flip_bijective_iff₁`, `flip_bijective_iff₂`, `flip_injective_iff₁`, `flip_injective_iff₂`, `flip_surjective_iff₁`, `flip_surjective_iff₂`, `range_dualMap_eq_dualAnnihilator_ker`, `range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective`, `range_dualMap_eq_dualAnnihilator_ker_of_surjective`, `dual_rank_eq`, `eq_of_ker_eq_of_apply_eq`, `finrank_ker_add_one_of_ne_zero`, `isCompl_ker_of_disjoint_of_ne_bot`, `range_eq_top_of_ne_zero`, `of_finite_of_free`, `exists_dual_eq_one`, `exists_dual_ne_zero`, `comap_eval_surjective`, `dualProdDualEquivDual_apply`, `dualProdDualEquivDual_apply_apply`, `dualProdDualEquivDual_symm_apply`, `dual_finite`, `dual_free`, `dual_projective`, `dual_rank_eq`, `eval_apply_eq_zero_iff`, `eval_apply_injective`, `eval_ker`, `exists_dual_forall_apply_eq_one`, `finite_dual_iff`, `forall_dual_apply_eq_zero_iff`, `instFiniteDimensionalOfIsReflexive`, `instIsReflexiveOfFiniteOfProjective`, `instNontrivialDual`, `map_eval_injective`, `nontrivial_dual_iff`, `subsingleton_dual_iff`, `instModuleIsReflexive`, `dualAnnihilator_eq_bot_iff`, `dualAnnihilator_eq_bot_iff'`, `dualAnnihilator_eq_top_iff`, `dualCoannihilator_top`, `dualCopairing_apply`, `dualCopairing_eq`, `dualPairing_apply`, `dualQuotEquivDualAnnihilator_apply`, `dualQuotEquivDualAnnihilator_symm_apply_mk`, `exists_dual_map_eq_bot_of_lt_top`, `exists_dual_map_eq_bot_of_notMem`, `finite_dualAnnihilator_iff`, `flip_quotDualCoannihilatorToDual_injective`, `quotDualCoannihilatorToDual_apply`, `quotDualCoannihilatorToDual_injective`, `quotDualCoannihilatorToDual_nondegenerate`, `range_dualMap_mkQ_eq`, `span_eq_top_of_ne_zero`, `comap_dualAnnihilator_dualAnnihilator`, `dualAnnihilator_dualAnnihilator_eq`, `dualAnnihilator_dualAnnihilator_eq_map`, `dualAnnihilator_dualCoannihilator_eq`, `dualAnnihilator_iInf_eq`, `dualAnnihilator_inf_eq`, `dualAnnihilator_inj`, `dualAnnihilator_le_dualAnnihilator_iff`, `dualCoannihilator_dualAnnihilator_eq`, `dualCopairing_nondegenerate`, `dualEquivDual_apply`, `dualEquivDual_def`, `dualLift_injective`, `dualLift_of_mem`, `dualLift_of_subtype`, `dualLift_rightInverse`, `dualPairing_eq`, `dualPairing_nondegenerate`, `dualRestrict_comp_dualLift`, `dualRestrict_leftInverse`, `dualRestrict_surjective`, `dual_finrank_eq`, `finiteDimensional_quot_dualCoannihilator_iff`, `finrank_add_finrank_dualAnnihilator_eq`, `finrank_add_finrank_dualCoannihilator_eq`, `finrank_dualCoannihilator_eq`, `flip_quotDualCoannihilatorToDual_bijective`, `forall_mem_dualAnnihilator_apply_eq_zero_iff`, `instModuleDualFiniteDimensional`, `isCompl_dualAnnihilator`, `map_dualCoannihilator`, `map_le_dualAnnihilator_dualAnnihilator`, `quotAnnihilatorEquiv_apply`, `quotDualCoannihilatorToDual_bijective`, `dualDistrib_apply`, `dualDistribEquivOfBasis_apply_apply`, `dualDistribEquivOfBasis_symm_apply`, `dualDistribInvOfBasis_apply`, `dualDistrib_apply`, `dualDistrib_apply_comm`, `dualDistrib_dualDistribInvOfBasis_left_inverse`, `dualDistrib_dualDistribInvOfBasis_right_inverse`, `instModuleIsReflexive`, `mem_span_of_iInf_ker_le_ker`, `span_flip_eq_top_iff_linearIndependent`	110
Total	130

Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearEquiv_dual_iff_finiteDimensional` 📖	mathematical	—	`LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Dual` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `FiniteDimensional` `Field.toDivisionRing`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `FiniteDimensional.eq_1` `Module.rank_lt_aleph0_iff` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `LT.lt.ne` `lift_rank_lt_rank_dual` `LinearEquiv.lift_rank_eq` `Cardinal.lift_id'` `Cardinal.lift_umax` `Finite.of_fintype`

FiniteDimensional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_span_of_iInf_ker_le_ker` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `iInf` `Submodule.instInfSet` `LinearMap.ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring`	`LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	—	`Algebra.to_smulCommClass` `RingHomSurjective.ids` `Submodule.exists_dual_map_eq_bot_of_notMem` `Module.Projective.of_free` `Module.Free.of_divisionRing` `RingHomInvPair.ids` `smulCommClass_self` `Module.instIsReflexiveOfFiniteOfProjective` `Submodule.mem_iInf` `Submodule.mem_bot` `Submodule.mem_map` `Submodule.subset_span` `Module.apply_evalEquiv_symm_apply`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dualAnnihilator_ker_eq_range_flip` 📖	mathematical	—	`Submodule.dualAnnihilator` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `ker` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `addCommMonoid` `module` `Algebra.to_smulCommClass` `CommSemiring.toSemiring` `Algebra.id` `range` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `RingHomSurjective.ids` `flip`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `SMulCommClass.symm` `RingHomSurjective.ids` `RingHomCompTriple.ids` `RingHomInvPair.ids` `range_dualMap_eq_dualAnnihilator_ker` `range_comp_of_range_eq_top` `RingHomSurjective.invPair` `LinearEquiv.range`
`dualMap_bijective_iff` 📖	mathematical	—	`Function.Bijective` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instFunLike` `dualMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`smulCommClass_self`
`dualMap_injective_iff` 📖	mathematical	—	`Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instFunLike` `dualMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`smulCommClass_self` `Function.mtr` `RingHomSurjective.ids` `Submodule.exists_le_ker_of_lt_top` `lt_top_iff_ne_top` `range_eq_top` `ext` `dualMap_injective_of_surjective`
`dualMap_surjective_iff` 📖	mathematical	—	`Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instFunLike` `dualMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`smulCommClass_self` `RingHomSurjective.ids` `range_eq_top` `range_dualMap_eq_dualAnnihilator_ker` `Submodule.dualAnnihilator_bot` `ker_eq_bot`
`dualMap_surjective_of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	`Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `dualMap`	—	`RingHomCompTriple.ids` `smulCommClass_self` `exists_leftInverse_of_injective` `ker_eq_bot` `ext`
`dualPairing_nondegenerate` 📖	mathematical	—	`Nondegenerate` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `addCommMonoid` `RingHom.id` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Module.dualPairing`	—	`smulCommClass_self` `separatingLeft_iff_ker_eq_bot` `ker_id` `Module.forall_dual_apply_eq_zero_iff` `Module.Projective.of_free` `Module.Free.of_divisionRing`
`finrank_range_dualMap_eq_finrank_range` 📖	mathematical	—	`Module.finrank` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Submodule` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `SetLike.instMembership` `Submodule.setLike` `range` `RingHomSurjective.ids` `dualMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`smulCommClass_self` `RingHomSurjective.ids` `RingHomCompTriple.ids` `dualMap_comp_dualMap` `range_comp` `range_eq_top` `dualMap_surjective_of_injective` `Submodule.injective_subtype` `Submodule.map_top` `dualMap_injective_of_surjective` `range_rangeRestrict` `Algebra.to_smulCommClass` `Subspace.dual_finrank_eq`
`flip_bijective_iff₁` 📖	mathematical	—	`Function.Bijective` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `DFunLike.coe` `addCommMonoid` `module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `instFunLike` `flip`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm`
`flip_bijective_iff₂` 📖	mathematical	—	`Function.Bijective` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `DFunLike.coe` `addCommMonoid` `module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `instFunLike` `flip`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm` `flip_bijective_iff₁`
`flip_injective_iff₁` 📖	mathematical	—	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `DFunLike.coe` `addCommMonoid` `module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `instFunLike` `flip`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm` `smulCommClass_self` `dualMap_surjective_iff` `RingHomInvPair.ids` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `Module.Free.of_divisionRing` `Equiv.surjective_comp`
`flip_injective_iff₂` 📖	mathematical	—	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `DFunLike.coe` `addCommMonoid` `module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `instFunLike` `flip`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm` `smulCommClass_self` `dualMap_injective_iff` `Equiv.injective_comp` `RingHomInvPair.ids` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `Module.Free.of_divisionRing`
`flip_surjective_iff₁` 📖	mathematical	—	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `DFunLike.coe` `addCommMonoid` `module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `instFunLike` `flip`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm` `flip_injective_iff₂`
`flip_surjective_iff₂` 📖	mathematical	—	`LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `DFunLike.coe` `addCommMonoid` `module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `instFunLike` `flip`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm` `flip_injective_iff₁`
`range_dualMap_eq_dualAnnihilator_ker` 📖	mathematical	—	`range` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHomSurjective.ids` `dualMap` `Submodule.dualAnnihilator` `ker` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective` `dualMap_surjective_of_injective` `RingHomSurjective.ids` `Submodule.injective_subtype`
`range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective` 📖	mathematical	`Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instFunLike` `dualMap` `Submodule.subtype`	`Submodule.dualAnnihilator` `ker`	—	`RingHomSurjective.ids` `smulCommClass_self` `range_eq_top` `range_rangeRestrict` `range_dualMap_eq_dualAnnihilator_ker_of_surjective` `RingHomCompTriple.ids` `range.congr_simp` `subtype_comp_codRestrict` `mem_range_self` `dualMap_comp_dualMap` `range_comp_of_range_eq_top` `ker_rangeRestrict`
`range_dualMap_eq_dualAnnihilator_ker_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	`range` `Module.Dual` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHomSurjective.ids` `dualMap` `Submodule.dualAnnihilator` `ker`	—	`smulCommClass_self` `RingHomSurjective.ids` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearEquiv.range_comp` `Submodule.range_dualMap_mkQ_eq`

Module

Definitions

Name	Category	Theorems
`dualProdDualEquivDual` 📖	CompOp	4 math math: `dualProdDualEquivDual_apply_apply`, `dualProdDualEquivDual_apply`, `dualProdDualEquivDual_symm_apply`, `QuadraticForm.dualProdProdIsometry_invFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_eval_surjective` 📖	mathematical	—	`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` `Submodule.comap` `Dual.eval`	—	`Submodule.comap_surjective_of_injective` `smulCommClass_self` `RingHomSurjective.ids` `eval_apply_injective`
`dualProdDualEquivDual_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Dual` `Prod.instAddCommMonoid` `Prod.instModule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `dualProdDualEquivDual` `LinearMap.coprod`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`dualProdDualEquivDual_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Prod.instModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Dual` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `dualProdDualEquivDual` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`dualProdDualEquivDual_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Dual` `Prod.instAddCommMonoid` `Prod.instModule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `dualProdDualEquivDual` `LinearMap` `LinearMap.comp` `LinearMap.inl` `LinearMap.inr`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`dual_finite` 📖	mathematical	—	`Finite` `Dual` `CommSemiring.toSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id`	—	`RingHomCompTriple.ids` `Algebra.to_smulCommClass` `Finite.exists_comp_eq_id_of_projective` `smulCommClass_self` `Finite.of_basis` `Free.function` `Finite.of_fintype` `Free.self` `Finite.pi` `Finite.self` `Finite.of_surjective` `RingHomSurjective.ids` `LinearMap.surjective_of_comp_eq_id` `RingHomInvPair.ids`
`dual_free` 📖	mathematical	—	`Free` `Dual` `CommSemiring.toSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id`	—	`Free.of_basis` `Algebra.to_smulCommClass` `Finite.of_fintype`
`dual_projective` 📖	mathematical	—	`Projective` `CommSemiring.toSemiring` `Dual` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id`	—	`RingHomCompTriple.ids` `Algebra.to_smulCommClass` `Finite.exists_comp_eq_id_of_projective` `Projective.of_split` `smulCommClass_self` `Projective.of_free` `dual_free` `Finite.pi` `Finite.of_fintype` `Finite.self` `Free.function` `Free.self`
`dual_rank_eq` 📖	mathematical	—	`rank` `Dual` `CommSemiring.toSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `Cardinal.lift`	—	`Basis.dual_rank_eq` `Finite.of_fintype`
`eval_apply_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Dual` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `toDistribMulAction` `LinearMap.instFunLike` `Dual.eval` `LinearMap.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`smulCommClass_self` `SetLike.ext_iff` `eval_ker`
`eval_apply_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`	—	`RingHomCompTriple.ids` `smulCommClass_self` `projective_def'` `Function.Injective.of_comp` `Basis.eval_injective` `LinearMap.injective_of_comp_eq_id` `RingHomInvPair.ids`
`eval_ker` 📖	mathematical	—	`LinearMap.ker` `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` `Dual.eval` `Bot.bot` `Submodule` `Submodule.instBot`	—	`LinearMap.ker_eq_bot_of_injective` `smulCommClass_self` `eval_apply_injective`
`exists_dual_forall_apply_eq_one` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid`	`DFunLike.coe` `Dual` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`LinearIndepOn.id_image` `Set.subset_univ` `LinearIndepOn.linearIndepOn_extend` `Subtype.range_coe_subtype` `Submodule.span_univ` `LinearIndepOn.span_extend_eq_span` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `LinearIndepOn.subset_extend` `Set.mem_image_of_mem` `Basis.constr_basis`
`finite_dual_iff` 📖	mathematical	—	`Finite` `Dual` `CommSemiring.toSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id`	—	`Algebra.to_smulCommClass` `Free.exists_basis` `finite_or_infinite` `Finite.of_basis` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `IsNoetherian.finite` `isNoetherian_of_subsingleton` `Finite.exists_nat_not_surjective` `rankCondition_of_nontrivial_of_commSemiring` `RingHomInvPair.ids` `smulCommClass_self` `RingHomCompTriple.ids` `Function.Injective.surjective_comp_right` `Nontrivial.to_nonempty` `Function.Embedding.injective` `LinearEquiv.surjective` `dual_finite` `Projective.of_free`
`forall_dual_apply_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `Dual` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `Projective.exists_dual_ne_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`instFiniteDimensionalOfIsReflexive` 📖	mathematical	—	`FiniteDimensional` `Field.toDivisionRing`	—	`FiniteDimensional.eq_1` `rank_lt_aleph0_iff` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Free.of_divisionRing` `Algebra.to_smulCommClass` `lift_rank_lt_rank_dual` `Cardinal.lift_id'` `le_trans` `LT.lt.le` `lt_trans` `lift_rank_eq_of_equiv_equiv` `RingHomInvPair.ids` `smulCommClass_self` `SemilinearEquivClass.toAddEquivClass` `LinearEquiv.instSemilinearEquivClass` `Function.bijective_id` `LinearEquiv.map_smul` `lt_irrefl` `Cardinal.lift_umax`
`instIsReflexiveOfFiniteOfProjective` 📖	mathematical	—	`IsReflexive`	—	`Finite.exists_fin'` `RingHomCompTriple.ids` `projective_lifting_property` `IsReflexive.of_split` `IsReflexive.of_finite_of_free` `Finite.pi` `Finite.of_fintype` `Finite.self` `Free.function` `Free.self`
`instNontrivialDual` 📖	mathematical	—	`Nontrivial` `Dual` `CommSemiring.toSemiring`	—	`nontrivial_dual_iff`
`map_eval_injective` 📖	mathematical	—	`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` `Submodule.map` `RingHomSurjective.ids` `Dual.eval`	—	`Submodule.map_injective_of_injective` `smulCommClass_self` `RingHomSurjective.ids` `eval_apply_injective`
`nontrivial_dual_iff` 📖	mathematical	—	`Nontrivial` `Dual` `CommSemiring.toSemiring`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `subsingleton_dual_iff`
`subsingleton_dual_iff` 📖	mathematical	—	`Dual` `CommSemiring.toSemiring`	—	`eval_apply_injective` `smulCommClass_self` `Unique.instSubsingleton`

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dual_rank_eq` 📖	mathematical	—	`Module.rank` `Module.Dual` `CommSemiring.toSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `Cardinal.lift`	—	`Algebra.to_smulCommClass` `Cardinal.lift_umax` `smulCommClass_self` `LinearEquiv.lift_rank_eq` `Cardinal.lift_id'`

Module.Dual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_ker_eq_of_apply_eq` 📖	—	`LinearMap.ker` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `DFunLike.coe` `Module.Dual` `LinearMap.instFunLike`	—	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `disjoint_iff` `Submodule.eq_bot_iff` `Submodule.mem_span_singleton` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `IsDomain.to_noZeroDivisors` `DivisionRing.isDomain` `zero_smul` `LinearMap.ext` `Submodule.mem_top` `Submodule.mem_sup` `IsCompl.sup_eq_top` `isCompl_ker_of_disjoint_of_ne_bot` `LinearMap.mem_ker` `map_add` `SemilinearMapClass.toAddHomClass` `zero_add`
`finrank_ker_add_one_of_ne_zero` 📖	mathematical	—	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearMap.ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `range_eq_top_of_ne_zero` `finrank_top` `Module.finrank_self` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `Submodule.finrank_quotient_add_finrank` `DivisionRing.hasRankNullity` `add_comm` `AddRightCancelSemigroup.toIsRightCancelAdd` `LinearEquiv.finrank_eq`
`isCompl_ker_of_disjoint_of_ne_bot` 📖	mathematical	`Disjoint` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `Submodule.instOrderBot` `LinearMap.ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id`	`IsCompl` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	—	`codisjoint_iff` `Submodule.eq_of_le_of_finrank_le` `Module.Finite.top` `le_top` `Submodule.finrank_sup_add_finrank_inf_eq` `FiniteDimensional.finiteDimensional_submodule` `DivisionRing.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `Submodule.finiteDimensional_inf_right` `Disjoint.eq_bot` `finrank_top` `finrank_ker_add_one_of_ne_zero` `add_le_add_iff_left` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Submodule.one_le_finrank_iff`
`range_eq_top_of_ne_zero` 📖	mathematical	—	`LinearMap.range` `DivisionSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomSurjective.ids` `Top.top` `Submodule` `Submodule.instTop`	—	`RingHomSurjective.ids` `LinearMap.range_eq_top` `LinearMap.surjective`

Module.IsReflexive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finite_of_free` 📖	mathematical	—	`Module.IsReflexive`	—	`smulCommClass_self` `Module.Basis.eval_injective` `RingHomSurjective.ids` `LinearMap.range_eq_top` `Module.Basis.eval_range` `Finite.of_fintype`

Module.Projective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_dual_eq_one` 📖	mathematical	—	`DFunLike.coe` `Module.Dual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`exists_dual_ne_zero` `Algebra.to_smulCommClass` `inv_mul_cancel₀`
`exists_dual_ne_zero` 📖	—	—	—	—	`RingHomCompTriple.ids` `iff_split` `Iff.not` `LinearMap.map_eq_zero_iff` `LinearMap.injective_of_comp_eq_id` `RingHomInvPair.ids` `LinearEquiv.map_ne_zero_iff` `Finsupp.ext`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instModuleIsReflexive` 📖	mathematical	—	`Module.IsReflexive` `instAddCommMonoid` `instModule` `CommSemiring.toSemiring`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass` `smulCommClass_self` `RingHomCompTriple.ids` `LinearMap.prod_ext` `LinearMap.ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `add_zero` `zero_add` `Function.Bijective.prodMap` `Module.bijective_dual_eval`

Submodule

Definitions

Name	Category	Theorems
`dualCopairing` 📖	CompOp	3 math math: `dualCopairing_eq`, `dualCopairing_apply`, `Subspace.dualCopairing_nondegenerate`
`dualPairing` 📖	CompOp	3 math math: `dualPairing_apply`, `Subspace.dualPairing_nondegenerate`, `Subspace.dualPairing_eq`
`dualQuotEquivDualAnnihilator` 📖	CompOp	3 math math: `dualQuotEquivDualAnnihilator_apply`, `dualCopairing_eq`, `dualQuotEquivDualAnnihilator_symm_apply_mk`
`instFunLikeSubtypeDualMemDualAnnihilator` 📖	CompOp	3 math math: `dualQuotEquivDualAnnihilator_apply`, `dualCopairing_apply`, `dualQuotEquivDualAnnihilator_symm_apply_mk`
`quotDualCoannihilatorToDual` 📖	CompOp	6 math math: `quotDualCoannihilatorToDual_apply`, `quotDualCoannihilatorToDual_nondegenerate`, `Subspace.flip_quotDualCoannihilatorToDual_bijective`, `quotDualCoannihilatorToDual_injective`, `Subspace.quotDualCoannihilatorToDual_bijective`, `flip_quotDualCoannihilatorToDual_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dualAnnihilator_eq_bot_iff` 📖	mathematical	—	`dualAnnihilator` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `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`	—	`smulCommClass_self` `dualAnnihilator_eq_bot_iff'` `Module.subsingleton_dual_iff` `Quotient.subsingleton_iff`
`dualAnnihilator_eq_bot_iff'` 📖	mathematical	—	`dualAnnihilator` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `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` `HasQuotient.Quotient` `hasQuotient` `CommRing.toRing` `Quotient.addCommGroup` `Quotient.module`	—	`smulCommClass_self` `Equiv.subsingleton_congr` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `subsingleton_iff_eq_bot`
`dualAnnihilator_eq_top_iff` 📖	mathematical	—	`dualAnnihilator` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Top.top` `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` `instTop` `Bot.bot` `instBot`	—	`smulCommClass_self` `eq_bot_iff` `Module.forall_dual_apply_eq_zero_iff` `mem_dualAnnihilator` `dualAnnihilator_bot`
`dualCoannihilator_top` 📖	mathematical	—	`dualCoannihilator` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Top.top` `Submodule` `Module.Dual` `CommSemiring.toSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `instTop` `Bot.bot` `instBot`	—	`Algebra.to_smulCommClass` `dualCoannihilator.eq_1` `smulCommClass_self` `dualAnnihilator_top` `comap_bot` `Module.eval_ker`
`dualCopairing_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `HasQuotient.Quotient` `Submodule` `AddCommGroup.toAddCommMonoid` `hasQuotient` `CommRing.toRing` `Quotient.addCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.module` `Semiring.toModule` `LinearMap.instFunLike` `Module.Dual` `LinearMap.addCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `SetLike.instMembership` `setLike` `dualAnnihilator` `addCommMonoid` `module` `Algebra.to_smulCommClass` `Algebra.id` `dualCopairing` `instFunLikeSubtypeDualMemDualAnnihilator`	—	`smulCommClass_self` `Algebra.to_smulCommClass`
`dualCopairing_eq` 📖	mathematical	—	`dualCopairing` `LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Dual` `AddCommGroup.toAddCommMonoid` `Submodule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `SetLike.instMembership` `setLike` `dualAnnihilator` `HasQuotient.Quotient` `hasQuotient` `CommRing.toRing` `Quotient.addCommGroup` `Quotient.module` `addCommMonoid` `module` `Algebra.to_smulCommClass` `Algebra.id` `LinearEquiv.symm` `dualQuotEquivDualAnnihilator`	—	`smulCommClass_self` `Algebra.to_smulCommClass`
`dualPairing_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `module` `Semiring.toModule` `LinearMap.instFunLike` `HasQuotient.Quotient` `Module.Dual` `LinearMap.addCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `hasQuotient` `CommRing.toRing` `LinearMap.addCommGroup` `Ring.toAddCommGroup` `dualAnnihilator` `Quotient.addCommGroup` `Quotient.module` `Algebra.to_smulCommClass` `Algebra.id` `dualPairing`	—	`smulCommClass_self` `Algebra.to_smulCommClass`
`dualQuotEquivDualAnnihilator_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `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` `instFunLikeSubtypeDualMemDualAnnihilator` `LinearEquiv` `RingHomInvPair.ids` `HasQuotient.Quotient` `hasQuotient` `CommRing.toRing` `Quotient.addCommGroup` `Quotient.module` `addCommMonoid` `Algebra.to_smulCommClass` `Algebra.id` `module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `dualQuotEquivDualAnnihilator` `LinearMap.instFunLike`	—	`smulCommClass_self` `RingHomInvPair.ids` `Algebra.to_smulCommClass`
`dualQuotEquivDualAnnihilator_symm_apply_mk` 📖	mathematical	—	`DFunLike.coe` `Module.Dual` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `CommRing.toRing` `Quotient.addCommGroup` `Quotient.module` `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` `SetLike.instMembership` `setLike` `dualAnnihilator` `addCommMonoid` `module` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `dualQuotEquivDualAnnihilator` `instFunLikeSubtypeDualMemDualAnnihilator`	—	`smulCommClass_self` `RingHomInvPair.ids` `Algebra.to_smulCommClass`
`exists_dual_map_eq_bot_of_lt_top` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Top.top` `instTop`	`map` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomSurjective.ids` `Bot.bot` `instBot`	—	`RingHomSurjective.ids` `Mathlib.Tactic.Contrapose.contrapose₂` `ext` `lt_top_iff_ne_top` `exists_dual_map_eq_bot_of_notMem`
`exists_dual_map_eq_bot_of_notMem` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike`	`map` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomSurjective.ids` `Bot.bot` `instBot`	—	`Module.Projective.exists_dual_ne_zero` `mkQ_apply` `Quotient.mk_eq_zero` `RingHomSurjective.ids` `RingHomCompTriple.ids` `map_comp` `map.congr_simp` `mkQ_map_self` `map_bot`
`finite_dualAnnihilator_iff` 📖	mathematical	—	`Module.Finite` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `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` `addCommMonoid` `module` `HasQuotient.Quotient` `hasQuotient` `CommRing.toRing` `Quotient.addCommGroup` `Quotient.module`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `Module.Finite.equiv_iff` `RingHomInvPair.ids` `Module.finite_dual_iff`
`flip_quotDualCoannihilatorToDual_injective` 📖	mathematical	—	`Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `SetLike.instMembership` `setLike` `LinearMap` `HasQuotient.Quotient` `hasQuotient` `CommRing.toRing` `dualCoannihilator` `Quotient.addCommGroup` `Quotient.module` `DFunLike.coe` `addCommMonoid` `module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `LinearMap.instFunLike` `LinearMap.flip` `quotDualCoannihilatorToDual`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm` `LinearMap.ext` `DFunLike.congr_fun`
`quotDualCoannihilatorToDual_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `LinearMap.instFunLike` `LinearMap` `HasQuotient.Quotient` `hasQuotient` `CommRing.toRing` `dualCoannihilator` `Quotient.addCommGroup` `Quotient.module` `quotDualCoannihilatorToDual`	—	`Algebra.to_smulCommClass`
`quotDualCoannihilatorToDual_injective` 📖	mathematical	—	`HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `CommRing.toRing` `dualCoannihilator` `Module.Dual` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `DFunLike.coe` `LinearMap` `Quotient.addCommGroup` `Quotient.module` `LinearMap.instFunLike` `quotDualCoannihilatorToDual`	—	`Algebra.to_smulCommClass` `LinearMap.ker_eq_bot` `ker_liftQ_eq_bot` `le_rfl`
`quotDualCoannihilatorToDual_nondegenerate` 📖	mathematical	—	`LinearMap.Nondegenerate` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `CommRing.toRing` `dualCoannihilator` `Module.Dual` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `SetLike.instMembership` `setLike` `Quotient.addCommGroup` `Quotient.module` `addCommMonoid` `module` `quotDualCoannihilatorToDual`	—	`Algebra.to_smulCommClass` `LinearMap.Nondegenerate.eq_1` `smulCommClass_self` `LinearMap.separatingLeft_iff_ker_eq_bot` `SMulCommClass.symm` `LinearMap.separatingRight_iff_flip_ker_eq_bot` `quotDualCoannihilatorToDual_injective` `flip_quotDualCoannihilatorToDual_injective`
`range_dualMap_mkQ_eq` 📖	mathematical	—	`LinearMap.range` `Module.Dual` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `hasQuotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Quotient.addCommGroup` `Quotient.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` `RingHomSurjective.ids` `LinearMap.dualMap` `mkQ` `dualAnnihilator`	—	`ext` `smulCommClass_self` `RingHomSurjective.ids` `LinearMap.mem_range` `LinearMap.mem_range_self` `ker_mkQ` `LinearMap.range_dualMap_le_dualAnnihilator_ker` `Algebra.to_smulCommClass`
`span_eq_top_of_ne_zero` 📖	mathematical	`LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `Set` `Set.instMembership`	`span` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `Top.top` `Submodule` `instTop`	—	`Algebra.to_smulCommClass` `RingHomSurjective.ids` `exists_dual_map_eq_bot_of_lt_top` `Ne.lt_top` `RingHomInvPair.ids` `smulCommClass_self` `mem_bot` `mem_map` `subset_span` `Module.apply_evalEquiv_symm_apply` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`

Subspace

Definitions

Name	Category	Theorems
`dualAnnihilatorGci` 📖	CompOp	—
`dualEquivDual` 📖	CompOp	2 math math: `dualEquivDual_def`, `dualEquivDual_apply`
`dualLift` 📖	CompOp	8 math math: `dualLift_of_subtype`, `dualRestrict_comp_dualLift`, `dualRestrict_leftInverse`, `dualLift_of_mem`, `dualEquivDual_def`, `dualLift_rightInverse`, `dualLift_injective`, `dualEquivDual_apply`
`dualQuotDistrib` 📖	CompOp	—
`orderIsoFiniteCodimDim` 📖	CompOp	—
`orderIsoFiniteDimensional` 📖	CompOp	—
`quotAnnihilatorEquiv` 📖	CompOp	2 math math: `quotAnnihilatorEquiv_apply`, `dualPairing_eq`
`quotDualEquivAnnihilator` 📖	CompOp	—
`quotEquivAnnihilator` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_dualAnnihilator_dualAnnihilator` 📖	mathematical	—	`Submodule.comap` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `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` `Submodule.dualAnnihilator`	—	`Submodule.ext` `smulCommClass_self` `forall_mem_dualAnnihilator_apply_eq_zero_iff`
`dualAnnihilator_dualAnnihilator_eq` 📖	mathematical	—	`Submodule.dualAnnihilator` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `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` `OrderIso` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `instFunLikeOrderIso` `Module.mapEvalEquiv` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `Module.Free.of_divisionRing` `Field.toDivisionRing`	—	`dualAnnihilator_dualCoannihilator_eq` `smulCommClass_self` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `Module.Free.of_divisionRing` `OrderIso.symm_apply_eq` `Module.mapEvalEquiv_symm_apply` `Submodule.dualCoannihilator.eq_1`
`dualAnnihilator_dualAnnihilator_eq_map` 📖	mathematical	—	`Submodule.dualAnnihilator` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `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` `Submodule.map` `RingHomSurjective.ids` `Module.Dual.eval`	—	`RingHomInvPair.ids` `smulCommClass_self` `RingHomCompTriple.ids` `Module.Free.of_divisionRing` `Finite.of_fintype` `Algebra.to_smulCommClass` `LinearEquiv.finiteDimensional` `RingHomSurjective.ids` `Submodule.eq_of_le_of_finrank_eq` `map_le_dualAnnihilator_dualAnnihilator` `RingHomSurjective.invPair` `LinearEquiv.finrank_eq` `Module.eval_apply_injective` `Module.Projective.of_free`
`dualAnnihilator_dualCoannihilator_eq` 📖	mathematical	—	`Submodule.dualCoannihilator` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Submodule.dualAnnihilator`	—	`le_antisymm` `Function.mtr` `smulCommClass_self` `Submodule.Quotient.mk_eq_zero` `Module.forall_dual_apply_eq_zero_iff` `Module.Projective.of_free` `Module.Free.of_divisionRing` `Mathlib.Tactic.Push.not_forall_eq` `RingHomCompTriple.ids` `LinearMap.comp_apply` `Submodule.mkQ_apply` `LinearMap.map_zero` `Submodule.le_dualAnnihilator_dualCoannihilator`
`dualAnnihilator_iInf_eq` 📖	mathematical	—	`Submodule.dualAnnihilator` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `iInf` `Subspace` `Field.toDivisionRing` `Submodule.instInfSet` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `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` `Submodule.completeLattice`	—	`Finite.induction_empty_option` `smulCommClass_self` `Equiv.iInf_comp` `Equiv.iSup_comp` `iSup_of_empty'` `PEmpty.instIsEmpty` `iInf_of_isEmpty` `sInf_empty` `sSup_empty` `Submodule.dualAnnihilator_top` `iInf_option` `iSup_option` `dualAnnihilator_inf_eq`
`dualAnnihilator_inf_eq` 📖	mathematical	—	`Submodule.dualAnnihilator` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Subspace` `Field.toDivisionRing` `Submodule.instMin` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `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` `Submodule.completeLattice`	—	`le_antisymm` `smulCommClass_self` `LinearMap.ker_prod` `Submodule.ker_mkQ` `RingHomSurjective.ids` `LinearMap.range_dualMap_eq_dualAnnihilator_ker` `LinearMap.mem_range` `Submodule.mem_sup` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `LinearEquiv.surjective` `Submodule.sup_dualAnnihilator_le_inf`
`dualAnnihilator_inj` 📖	mathematical	—	`Submodule.dualAnnihilator` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid`	—	`smulCommClass_self` `GaloisCoinsertion.l_injective`
`dualAnnihilator_le_dualAnnihilator_iff` 📖	mathematical	—	`Submodule` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `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` `Submodule.instPartialOrder` `Submodule.dualAnnihilator` `Subspace` `Field.toDivisionRing` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring`	—	`GaloisCoinsertion.l_le_l_iff` `smulCommClass_self`
`dualCoannihilator_dualAnnihilator_eq` 📖	mathematical	—	`Submodule.dualAnnihilator` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Submodule.dualCoannihilator`	—	`Algebra.to_smulCommClass` `RingHomInvPair.ids` `smulCommClass_self` `SMulCommClass.symm` `RingHomCompTriple.ids` `flip_quotDualCoannihilatorToDual_bijective` `Submodule.eq_of_le_of_finrank_eq` `LinearEquiv.finiteDimensional` `Submodule.le_dualCoannihilator_dualAnnihilator` `LinearEquiv.finrank_eq`
`dualCopairing_nondegenerate` 📖	mathematical	—	`LinearMap.Nondegenerate` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `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` `Submodule.setLike` `Submodule.dualAnnihilator` `HasQuotient.Quotient` `Submodule.hasQuotient` `CommRing.toRing` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Submodule.addCommMonoid` `Submodule.module` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.dualCopairing`	—	`smulCommClass_self` `LinearMap.separatingLeft_iff_ker_eq_bot` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `Submodule.dualCopairing_eq` `LinearEquiv.ker` `forall_mem_dualAnnihilator_apply_eq_zero_iff` `SetLike.forall`
`dualEquivDual_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Dual` `Subspace` `Field.toDivisionRing` `SetLike.instMembership` `Submodule.setLike` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.addCommMonoid` `Submodule.module` `Submodule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `LinearMap.range` `RingHomSurjective.ids` `dualLift` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `dualEquivDual` `LinearMap` `LinearMap.instFunLike` `LinearMap.mem_range`	—	`Algebra.to_smulCommClass` `RingHomSurjective.ids` `RingHomInvPair.ids`
`dualEquivDual_def` 📖	mathematical	—	`LinearEquiv.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Dual` `Subspace` `Field.toDivisionRing` `SetLike.instMembership` `Submodule.setLike` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.addCommMonoid` `Submodule.module` `Submodule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `LinearMap.range` `RingHomSurjective.ids` `dualLift` `dualEquivDual` `LinearMap.rangeRestrict`	—	`Algebra.to_smulCommClass` `RingHomSurjective.ids` `RingHomInvPair.ids`
`dualLift_injective` 📖	mathematical	—	`Module.Dual` `Subspace` `Field.toDivisionRing` `SetLike.instMembership` `Submodule.setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Semifield.toDivisionSemiring` `Field.toSemifield` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `LinearMap.instFunLike` `dualLift`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `dualRestrict_leftInverse`
`dualLift_of_mem` 📖	mathematical	`Subspace` `Field.toDivisionRing` `SetLike.instMembership` `Submodule.setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`DFunLike.coe` `Module.Dual` `Semifield.toDivisionSemiring` `Field.toSemifield` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `dualLift`	—	`dualLift_of_subtype`
`dualLift_of_subtype` 📖	mathematical	—	`DFunLike.coe` `Module.Dual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap` `Subspace` `Field.toDivisionRing` `SetLike.instMembership` `Submodule.setLike` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `dualLift`	—	`Submodule.ker_subtype`
`dualLift_rightInverse` 📖	mathematical	—	`Module.Dual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Subspace` `Field.toDivisionRing` `SetLike.instMembership` `Submodule.setLike` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `LinearMap.instFunLike` `dualLift` `Submodule` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.dualRestrict`	—	`dualRestrict_leftInverse`
`dualPairing_eq` 📖	mathematical	—	`Submodule.dualPairing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearEquiv.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `HasQuotient.Quotient` `Module.Dual` `AddCommGroup.toAddCommMonoid` `Submodule` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.hasQuotient` `DivisionRing.toRing` `Field.toDivisionRing` `LinearMap.addCommGroup` `Ring.toAddCommGroup` `Submodule.dualAnnihilator` `Subspace` `SetLike.instMembership` `Submodule.setLike` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Algebra.to_smulCommClass` `Algebra.id` `quotAnnihilatorEquiv`	—	`Submodule.linearMap_qext` `smulCommClass_self` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `LinearMap.ext` `RingHomCompTriple.ids`
`dualPairing_nondegenerate` 📖	mathematical	—	`LinearMap.Nondegenerate` `HasQuotient.Quotient` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `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` `Submodule.hasQuotient` `CommRing.toRing` `LinearMap.addCommGroup` `Ring.toAddCommGroup` `Submodule.dualAnnihilator` `SetLike.instMembership` `Submodule.setLike` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.addCommMonoid` `Submodule.module` `Submodule.dualPairing`	—	`smulCommClass_self` `LinearMap.separatingLeft_iff_ker_eq_bot` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `dualPairing_eq` `LinearEquiv.ker` `Module.forall_dual_apply_eq_zero_iff` `Module.Projective.of_free` `Module.Free.of_divisionRing` `dualLift_of_subtype`
`dualRestrict_comp_dualLift` 📖	mathematical	—	`LinearMap.comp` `Module.Dual` `Subspace` `Field.toDivisionRing` `SetLike.instMembership` `Submodule.setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Semifield.toDivisionSemiring` `Field.toSemifield` `Submodule.addCommMonoid` `Submodule.module` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Submodule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHomCompTriple.ids` `Submodule.dualRestrict` `dualLift` `LinearMap` `Module.End.instOne`	—	`LinearMap.ext` `Algebra.to_smulCommClass` `smulCommClass_self` `RingHomCompTriple.ids` `dualLift_of_subtype`
`dualRestrict_leftInverse` 📖	mathematical	—	`Module.Dual` `Submodule` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `Submodule.dualRestrict` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subspace` `Field.toDivisionRing` `DivisionRing.toDivisionSemiring` `Algebra.to_smulCommClass` `Algebra.id` `dualLift`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `LinearMap.comp_apply` `dualRestrict_comp_dualLift` `Module.End.one_apply`
`dualRestrict_surjective` 📖	mathematical	—	`Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `Submodule.dualRestrict`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `dualLift_rightInverse`
`dual_finrank_eq` 📖	mathematical	—	`Module.finrank` `Module.Dual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`Algebra.to_smulCommClass` `LinearEquiv.finrank_eq` `smulCommClass_self` `RingHomInvPair.ids` `Finite.of_fintype` `finrank_eq_zero_of_basis_imp_false` `Module.Free.of_divisionRing` `Module.finite_dual_iff` `Module.Finite.of_basis`
`finiteDimensional_quot_dualCoannihilator_iff` 📖	mathematical	—	`FiniteDimensional` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `DivisionRing.toRing` `Field.toDivisionRing` `Submodule.dualCoannihilator` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Module.Dual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `LinearMap.addCommGroup` `Ring.toAddCommGroup` `Submodule.module`	—	`Algebra.to_smulCommClass` `FiniteDimensional.of_injective` `SMulCommClass.symm` `Submodule.flip_quotDualCoannihilatorToDual_injective` `instModuleDualFiniteDimensional` `Submodule.quotDualCoannihilatorToDual_injective`
`finrank_add_finrank_dualAnnihilator_eq` 📖	mathematical	—	`Module.finrank` `Subspace` `Field.toDivisionRing` `SetLike.instMembership` `Submodule.setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Semifield.toDivisionSemiring` `Field.toSemifield` `Submodule.addCommMonoid` `Submodule.module` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `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` `Submodule.dualAnnihilator`	—	`smulCommClass_self` `LinearEquiv.finrank_eq` `add_comm` `Submodule.finrank_quotient_add_finrank` `DivisionRing.hasRankNullity` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`finrank_add_finrank_dualCoannihilator_eq` 📖	mathematical	—	`Module.finrank` `Module.Dual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Subspace` `Field.toDivisionRing` `LinearMap.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DivisionRing.toDivisionSemiring` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Submodule` `Submodule.dualCoannihilator`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `finrank_dualCoannihilator_eq` `finrank_add_finrank_dualAnnihilator_eq` `instModuleDualFiniteDimensional` `dual_finrank_eq`
`finrank_dualCoannihilator_eq` 📖	mathematical	—	`Module.finrank` `Submodule` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.dualCoannihilator` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module` `Module.Dual` `LinearMap.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DivisionRing.toDivisionSemiring` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.addCommMonoid` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.dualAnnihilator`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `Submodule.dualCoannihilator.eq_1` `RingHomInvPair.ids` `Module.instIsReflexiveOfFiniteOfProjective` `Module.Projective.of_free` `Module.Free.of_divisionRing` `Module.evalEquiv_toLinearMap` `LinearEquiv.finrank_eq`
`flip_quotDualCoannihilatorToDual_bijective` 📖	mathematical	—	`Function.Bijective` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `Submodule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `SetLike.instMembership` `Submodule.setLike` `LinearMap` `HasQuotient.Quotient` `Submodule.hasQuotient` `CommRing.toRing` `Submodule.dualCoannihilator` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `DFunLike.coe` `Submodule.addCommMonoid` `Submodule.module` `SMulCommClass.symm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `LinearMap.instFunLike` `LinearMap.flip` `Submodule.quotDualCoannihilatorToDual`	—	`Algebra.to_smulCommClass` `SMulCommClass.symm` `LinearMap.flip_bijective_iff₂` `quotDualCoannihilatorToDual_bijective`
`forall_mem_dualAnnihilator_apply_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `Module.Dual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subspace` `Field.toDivisionRing` `SetLike.instMembership` `Submodule.setLike` `DivisionRing.toDivisionSemiring`	—	`smulCommClass_self` `SetLike.ext_iff` `dualAnnihilator_dualCoannihilator_eq` `Submodule.mem_dualCoannihilator`
`instModuleDualFiniteDimensional` 📖	mathematical	—	`FiniteDimensional` `Module.Dual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Field.toDivisionRing` `LinearMap.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DivisionRing.toDivisionSemiring` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id`	—	`Algebra.to_smulCommClass` `Module.dual_finite` `Module.Projective.of_free` `Module.Free.of_divisionRing`
`isCompl_dualAnnihilator` 📖	mathematical	`IsCompl` `Subspace` `Field.toDivisionRing` `Submodule.instPartialOrder` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	`Submodule` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `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` `Submodule.dualAnnihilator`	—	`smulCommClass_self` `isCompl_iff` `disjoint_iff` `codisjoint_iff` `dualAnnihilator_inf_eq` `Submodule.dualAnnihilator_sup_eq` `Submodule.dualAnnihilator_top` `Submodule.dualAnnihilator_bot`
`map_dualCoannihilator` 📖	mathematical	—	`Submodule.map` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `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` `RingHomSurjective.ids` `Module.Dual.eval` `Submodule.dualCoannihilator` `Submodule.dualAnnihilator` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `LinearMap.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `DivisionRing.toDivisionSemiring` `Algebra.to_smulCommClass` `Algebra.id`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `RingHomSurjective.ids` `dualAnnihilator_dualAnnihilator_eq_map` `FiniteDimensional.finiteDimensional_submodule` `dualCoannihilator_dualAnnihilator_eq` `instModuleDualFiniteDimensional`
`map_le_dualAnnihilator_dualAnnihilator` 📖	mathematical	—	`Submodule` `Module.Dual` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `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` `Submodule.instPartialOrder` `Submodule.map` `RingHomSurjective.ids` `Module.Dual.eval` `Submodule.dualAnnihilator`	—	`smulCommClass_self` `RingHomSurjective.ids` `Submodule.map_le_iff_le_comap` `Eq.ge` `comap_dualAnnihilator_dualAnnihilator`
`quotAnnihilatorEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `HasQuotient.Quotient` `Module.Dual` `AddCommGroup.toAddCommMonoid` `Submodule` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.hasQuotient` `DivisionRing.toRing` `Field.toDivisionRing` `LinearMap.addCommGroup` `Ring.toAddCommGroup` `Submodule.dualAnnihilator` `Subspace` `SetLike.instMembership` `Submodule.setLike` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `quotAnnihilatorEquiv` `LinearMap` `LinearMap.instFunLike` `Submodule.dualRestrict`	—	`LinearMap.ext` `RingHomInvPair.ids` `smulCommClass_self` `Algebra.to_smulCommClass`
`quotDualCoannihilatorToDual_bijective` 📖	mathematical	—	`Function.Bijective` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Submodule.dualCoannihilator` `Module.Dual` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `LinearMap.instFunLike` `Submodule.quotDualCoannihilatorToDual`	—	`Algebra.to_smulCommClass` `Submodule.quotDualCoannihilatorToDual_injective` `SMulCommClass.symm` `LinearMap.flip_injective_iff₂` `Submodule.flip_quotDualCoannihilatorToDual_injective`

TensorProduct

Definitions

Name	Category	Theorems
`dualDistrib` 📖	CompOp	6 math math: `dualDistrib_dualDistribInvOfBasis_right_inverse`, `dualDistrib_apply_comm`, `dualDistrib_dualDistribInvOfBasis_left_inverse`, `map_dualTensorHom`, `dualDistrib_apply`, `PointedCone.mem_maxTensorProduct`
`dualDistribEquiv` 📖	CompOp	—
`dualDistribEquivOfBasis` 📖	CompOp	2 math math: `dualDistribEquivOfBasis_symm_apply`, `dualDistribEquivOfBasis_apply_apply`
`dualDistribInvOfBasis` 📖	CompOp	3 math math: `dualDistrib_dualDistribInvOfBasis_right_inverse`, `dualDistribInvOfBasis_apply`, `dualDistrib_dualDistribInvOfBasis_left_inverse`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dualDistribEquivOfBasis_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Module.Dual` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `dualDistribEquivOfBasis` `lid` `homTensorHomMap`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`dualDistribEquivOfBasis_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Module.Dual` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `dualDistribEquivOfBasis` `Finset.sum` `Finset.univ` `instSMul` `LinearMap.instFunLike` `tmul` `Module.Basis` `Module.Basis.instFunLike` `Module.Basis.coord`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `Finite.of_fintype` `dualDistribInvOfBasis_apply` `Finset.sum_congr` `Module.Basis.coe_dualBasis`
`dualDistribInvOfBasis_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.Dual` `TensorProduct` `addCommMonoid` `instModule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.instFunLike` `dualDistribInvOfBasis` `Finset.sum` `Finset.univ` `instSMul` `tmul` `Module.Basis` `Module.Basis.instFunLike` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Module.Basis.dualBasis` `Finite.of_fintype`	—	`Algebra.to_smulCommClass` `smulCommClass_self` `Finite.of_fintype` `Finset.sum_congr` `RingHomInvPair.ids` `LinearMap.comp.congr_simp` `Module.Basis.coe_dualBasis` `LinearMap.coe_sum` `Finset.sum_apply`
`dualDistrib_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Dual` `TensorProduct` `CommSemiring.toSemiring` `addCommMonoid` `instModule` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `dualDistrib` `tmul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Algebra.to_smulCommClass`
`dualDistrib_apply_comm` 📖	mathematical	—	`DFunLike.coe` `Module.Dual` `TensorProduct` `CommSemiring.toSemiring` `addCommMonoid` `instModule` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `dualDistrib` `LinearEquiv` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `comm`	—	`Algebra.to_smulCommClass` `induction_on` `RingHomInvPair.ids` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `map_add` `SemilinearMapClass.toAddHomClass` `mul_comm` `add_zero`
`dualDistrib_dualDistribInvOfBasis_left_inverse` 📖	mathematical	—	`LinearMap.comp` `Module.Dual` `TensorProduct` `CommSemiring.toSemiring` `addCommMonoid` `instModule` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `RingHomCompTriple.ids` `dualDistrib` `dualDistribInvOfBasis` `LinearMap.id`	—	`Module.Basis.ext` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `smulCommClass_self` `Finite.instProd` `Finite.of_fintype` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `Module.Basis.coe_dualBasis` `dualDistribInvOfBasis_apply` `Finset.sum_congr` `RingHomInvPair.ids` `Module.Basis.tensorProduct_repr_tmul_apply` `Module.Basis.repr_self` `smulCommClass_left` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Module.Basis.tensorProduct_apply` `LinearMap.coe_sum` `Finset.sum_apply` `Finset.sum_eq_single` `Finsupp.single_eq_of_ne'` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `Finset.sum_const_zero` `Finsupp.single_eq_same` `mul_one` `one_mul` `mul_comm`
`dualDistrib_dualDistribInvOfBasis_right_inverse` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `Module.Dual` `CommSemiring.toSemiring` `LinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `addCommMonoid` `instModule` `RingHomCompTriple.ids` `dualDistribInvOfBasis` `dualDistrib` `LinearMap.id`	—	`Module.Basis.ext` `Algebra.to_smulCommClass` `smulCommClass_self` `IsScalarTower.to_smulCommClass` `LinearMap.instIsScalarTower` `IsScalarTower.right` `Finite.of_fintype` `RingHomCompTriple.ids` `Module.Basis.tensorProduct_apply` `Module.Basis.coe_dualBasis` `dualDistribInvOfBasis_apply` `Finset.sum_congr` `RingHomInvPair.ids` `Module.Basis.repr_self` `Finset.sum_eq_single` `Finsupp.single_eq_of_ne'` `MulZeroClass.zero_mul` `zero_smul` `Finset.sum_const_zero` `Finsupp.single_eq_same` `MulZeroClass.mul_zero` `mul_one` `one_smul`

TensorProduct.AlgebraTensorModule

Definitions

Name	Category	Theorems
`dualDistrib` 📖	CompOp	1 math math: `dualDistrib_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dualDistrib_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Dual` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.toModule` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.instSMulCommClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `dualDistrib` `TensorProduct.tmul` `Algebra.toSMul`	—	`IsScalarTower.to_smulCommClass` `IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `Algebra.to_smulCommClass` `LinearMap.instSMulCommClass`

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instModuleIsReflexive` 📖	mathematical	—	`Module.IsReflexive` `addCommMonoid` `module'` `CommSemiring.toSemiring`	—	`Module.equiv` `RingHomInvPair.ids`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_span_of_iInf_ker_le_ker` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `iInf` `Submodule.instInfSet` `LinearMap.ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring`	`LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	—	`LinearMap.ker_pi` `Eq.le` `FiniteDimensional.of_injective` `LinearMap.ker_eq_bot` `Submodule.ker_liftQ_eq_bot'` `FiniteDimensional.finiteDimensional_pi'` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `iInf_le` `le_iInf` `Submodule.pi_liftQ_eq_liftQ_pi` `bot_le` `Algebra.to_smulCommClass` `Submodule.mem_span_range_iff_exists_fun` `FiniteDimensional.mem_span_of_iInf_ker_le_ker` `RingHomCompTriple.ids` `Submodule.liftQ_mkQ` `LinearMap.ext` `LinearMap.coe_sum` `Finset.sum_apply` `Finset.sum_congr` `LinearMap.congr_fun`
`span_flip_eq_top_iff_linearIndependent` 📖	mathematical	—	`Submodule.span` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Pi.Function.module` `Semiring.toModule` `Set.range` `Top.top` `Submodule` `Submodule.instTop` `LinearIndependent`	—	`linearIndependent_iff_ker` `Algebra.to_smulCommClass` `RingHomSurjective.ids` `RingHomInvPair.ids` `Submodule.map_eq_top_iff` `smulCommClass_self` `Subspace.dualCoannihilator_dualAnnihilator_eq` `FiniteDimensional.instSubtypeMemSubmoduleMap` `FiniteDimensional.finiteDimensional_submodule` `FiniteDimensional.finiteDimensional_pi'` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `Submodule.dualAnnihilator_eq_top_iff` `Module.Free.finsupp` `SetLike.ext'_iff` `Submodule.map_span` `Submodule.coe_dualCoannihilator_span` `Set.range_comp` `Set.ext` `Finset.sum_congr` `Finset.sum_apply`

---

← Back to Index