FixedSubmodule

📁 Source: Mathlib/LinearAlgebra/FixedSubmodule.lean

Statistics

Metric	Count
Definitions fixedReduce, reduce, fixedSubmodule	3
Theorems fixedReduce_eq_one, fixedReduce_eq_smul_iff, fixedReduce_mk, fixedReduce_mkQ, fixedSubmodule_eq_top_iff, map_eq_of_mem_fixingSubgroup, mem_stabilizer_fixedSubmodule, mem_stabilizer_submodule_of_le_fixedSubmodule, reduce_mk, reduce_mkQ, fixedSubmodule_comp_inf_fixedSubmodule_le, fixedSubmodule_eq_ker, fixedSubmodule_eq_top_iff, fixedSubmodule_inf_fixedSubmodule_le_comp, mem_fixedSubmodule_iff	15
Total	18

LinearEquiv

Definitions

Name	Category	Theorems
fixedReduce 📖	CompOp	5 math math: fixedReduce_eq_one, mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one, fixedReduce_eq_smul_iff, fixedReduce_mk, fixedReduce_mkQ
reduce 📖	CompOp	2 math math: reduce_mk, reduce_mkQ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fixedReduce_eq_one 📖	mathematical	—	fixedReduce refl HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient LinearMap.fixedSubmodule toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule.Quotient.addCommGroup Submodule.Quotient.module SetLike.instMembership Submodule.setLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DFunLike.coe LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv	—	RingHomInvPair.ids map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass instSemilinearEquivClass one_smul fixedReduce_eq_smul_iff
fixedReduce_eq_smul_iff 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient LinearMap.fixedSubmodule toLinearMap Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv fixedReduce Submodule.Quotient.instSMul SetLike.instMembership Submodule.setLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids Submodule.ker_mkQ map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass Submodule.mkQ_surjective
fixedReduce_mk 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient LinearMap.fixedSubmodule toLinearMap Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv fixedReduce	—	RingHomInvPair.ids
fixedReduce_mkQ 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient LinearMap.fixedSubmodule toLinearMap Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv fixedReduce LinearMap LinearMap.instFunLike Submodule.mkQ	—	RingHomInvPair.ids
fixedSubmodule_eq_top_iff 📖	mathematical	—	LinearMap.fixedSubmodule toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Top.top Submodule Submodule.instTop refl	—	RingHomInvPair.ids
map_eq_of_mem_fixingSubgroup 📖	mathematical	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Subgroup automorphismGroup SetLike.instMembership Subgroup.instSetLike fixingSubgroup DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommMonoid.toAddMonoid applyDistribMulAction AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddSubmonoid.toAddSubsemigroup Submodule.toAddSubmonoid	Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids toLinearMap RingHomInvPair.ids	—	RingHomInvPair.ids Submodule.ext RingHomSurjective.ids
mem_stabilizer_fixedSubmodule 📖	mathematical	—	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Subgroup automorphismGroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Submodule DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid Submodule.pointwiseDistribMulAction applyDistribMulAction apply_smulCommClass' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.left LinearMap.fixedSubmodule toLinearMap	—	RingHomInvPair.ids mem_stabilizer_submodule_of_le_fixedSubmodule le_refl
mem_stabilizer_submodule_of_le_fixedSubmodule 📖	mathematical	Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.fixedSubmodule toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Subgroup automorphismGroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Submodule DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid Submodule.pointwiseDistribMulAction applyDistribMulAction apply_smulCommClass' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.left	—	RingHomInvPair.ids apply_smulCommClass' IsScalarTower.left RingHomSurjective.ids Submodule.mem_stabilizer_submodule_iff_map_eq le_antisymm coe_toLinearMap LinearMap.mem_fixedSubmodule_iff
reduce_mk 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv MonoidHom Subgroup automorphismGroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid Submodule.pointwiseDistribMulAction applyDistribMulAction apply_smulCommClass' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.left MulOneClass.toMulOne Monoid.toMulOneClass Subgroup.toGroup MonoidHom.instFunLike reduce	—	RingHomInvPair.ids apply_smulCommClass' IsScalarTower.left
reduce_mkQ 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv MonoidHom Subgroup automorphismGroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid Submodule.pointwiseDistribMulAction applyDistribMulAction apply_smulCommClass' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.left MulOneClass.toMulOne Monoid.toMulOneClass Subgroup.toGroup MonoidHom.instFunLike reduce LinearMap LinearMap.instFunLike Submodule.mkQ	—	RingHomInvPair.ids apply_smulCommClass' IsScalarTower.left

LinearMap

Definitions

Name	Category	Theorems
fixedSubmodule 📖	CompOp	16 math math: LinearEquiv.ker_le_fixedSubmodule_transvection, fixedSubmodule_eq_top_iff, LinearEquiv.fixedReduce_eq_one, LinearEquiv.mem_fixedSubmodule_transvection_iff, LinearEquiv.fixedSubmodule_eq_top_iff, LinearEquiv.mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one, LinearEquiv.mem_dilatransvections_iff_rank_quotient, LinearEquiv.fixedReduce_eq_smul_iff, fixedSubmodule_comp_inf_fixedSubmodule_le, fixedSubmodule_eq_ker, LinearEquiv.mem_stabilizer_fixedSubmodule, mem_fixedSubmodule_iff, LinearEquiv.fixedReduce_mk, fixedSubmodule_inf_fixedSubmodule_le_comp, LinearEquiv.mem_dilatransvections_iff_finrank_quotient, LinearEquiv.fixedReduce_mkQ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fixedSubmodule_comp_inf_fixedSubmodule_le 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.instMin fixedSubmodule comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	RingHomCompTriple.ids
fixedSubmodule_eq_ker 📖	mathematical	—	fixedSubmodule Ring.toSemiring AddCommGroup.toAddCommMonoid ker RingHom.id Semiring.toNonAssocSemiring LinearMap instSub id	—	Submodule.ext
fixedSubmodule_eq_top_iff 📖	mathematical	—	fixedSubmodule Top.top Submodule Submodule.instTop id	—	—
fixedSubmodule_inf_fixedSubmodule_le_comp 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.instMin fixedSubmodule comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	RingHomCompTriple.ids
mem_fixedSubmodule_iff 📖	mathematical	—	Submodule SetLike.instMembership Submodule.setLike fixedSubmodule DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike	—	—

---

← Back to Index