Restrict

📁 Source: Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean

Statistics

Metric	Count
Definitions	0
Theorems restrict, restrictScalars, restrictScalars_of_field, exists_basis_basis_of_span_eq_top_of_mem_algebraMap, finrank_eq_of_isPerfPair, restrictScalarsField_apply_apply	6
Total	6

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_basis_basis_of_span_eq_top_of_mem_algebraMap 📖	mathematical	Submodule.span DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SetLike.coe Submodule Submodule.setLike Top.top Submodule.instTop Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id	Module.Basis Module.Basis.instFunLike Submodule.addCommMonoid Submodule.module	—	Algebra.to_smulCommClass Module.IsReflexive.of_isPerfPair flip.instIsPerfPair exists_linearIndependent Subtype.range_coe_subtype Set.setOf_mem_eq le_refl Module.Finite.finite_basis IsLocalRing.toNontrivial Field.instIsLocalRing Module.instFiniteDimensionalOfIsReflexive Subtype.coe_prop LinearIndependent.restrict_scalars FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing LinearIndependent.of_comp le_antisymm Submodule.span_le Module.finrank_eq_card_basis commRing_strongRankCondition Module.finrank_of_isPerfPair smulCommClass_self Finite.of_fintype RingHomInvPair.ids Module.Basis.dualBasis_repr Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left Module.Basis.toMatrix_mul_toMatrix Module.Basis.toMatrix_self Module.Basis.mem_span_iff_repr_mem instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Module.Basis.toMatrix_mulVec_repr Subring.sum_mem Subring.mul_mem Submodule.map_injective_of_injective RingHomSurjective.ids Submodule.injective_subtype Submodule.map_span Set.image_univ Set.image_image Set.image_congr Submodule.map_top Submodule.range_subtype Module.Basis.coe_reindex
finrank_eq_of_isPerfPair 📖	mathematical	Submodule.span DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SetLike.coe Submodule Submodule.setLike Top.top Submodule.instTop Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id	Module.finrank Submodule.addCommMonoid Submodule.module	—	Algebra.to_smulCommClass exists_basis_basis_of_span_eq_top_of_mem_algebraMap Module.finrank_eq_card_basis commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing
restrictScalarsField_apply_apply 📖	mathematical	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id	RingHom RingHom.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction restrictScalarsRange₂ Algebra.toSMul Algebra.toModule IsScalarTower.right IsScalarTower.to_smulCommClass' Algebra.linearMap FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing Ring.toAddCommGroup IsLocalRing.toNontrivial Field.instIsLocalRing	—	Algebra.to_smulCommClass restrictScalarsRange₂_apply IsScalarTower.right IsScalarTower.to_smulCommClass' FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing

LinearMap.IsPerfPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrict 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.IsPerfectCompl LinearMap.range RingHomSurjective.ids	LinearMap.IsPerfPair LinearMap.compl₁₂ NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass RingHomSurjective.ids LinearMap.flip.instIsPerfPair LinearMap.IsPerfectCompl.flip
restrictScalars 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike Submodule.span SetLike.coe Submodule Submodule.setLike LinearMap.range RingHomSurjective.ids Top.top Submodule.instTop LinearMap.comp NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule RingHomCompTriple.ids LinearMap.restrictScalars Semiring.toModule LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul IsScalarTower.right LinearEquiv RingHomInvPair.ids Module.Dual LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toPerfPair Algebra.linearMap LinearMap.flip NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LinearMap.flip.instIsPerfPair Subring CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap	LinearMap.IsPerfPair LinearMap.restrictScalarsRange₂ IsScalarTower.to_smulCommClass' FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero	—	Algebra.to_smulCommClass RingHomSurjective.ids RingHomCompTriple.ids LinearMap.IsScalarTower.compatibleSMul IsScalarTower.right RingHomInvPair.ids LinearMap.flip.instIsPerfPair IsScalarTower.to_smulCommClass' FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero SMulCommClass.symm
restrictScalars_of_field 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.IsPerfectCompl EuclideanDomain.toCommRing Field.toEuclideanDomain Submodule.span SetLike.coe Submodule Submodule.setLike LinearMap.range RingHomSurjective.ids Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id	LinearMap.IsPerfPair LinearMap.restrictScalarsRange₂ Algebra.toSMul NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right IsScalarTower.to_smulCommClass' Algebra.linearMap FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing Ring.toAddCommGroup IsLocalRing.toNontrivial Field.instIsLocalRing	—	Algebra.to_smulCommClass RingHomSurjective.ids restrict LinearMap.IsPerfectCompl.congr_simp Submodule.range_subtype Submodule.isScalarTower' IsScalarTower.left RingHomCompTriple.ids Submodule.injective_inclusionSpan LinearMap.range_comp_of_range_eq_top LinearMap.range_rangeRestrict Submodule.span_range_inclusionSpan LinearMap.BilinMap.apply_apply_mem_of_mem_span IsScalarTower.to_smulCommClass' IsScalarTower.right smulCommClass_self LinearMap.IsScalarTower.compatibleSMul LinearMap.instIsScalarTower Submodule.subset_span

---

← Back to Index