Pi

📁 Source: Mathlib/LinearAlgebra/Eigenspace/Pi.lean

Statistics

Metric	Count
Definitions	0
Theorems disjoint_iInf_maxGenEigenspace, iInf_maxGenEigenspace_restrict_map_subtype_eq, iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo, iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute, independent_iInf_maxGenEigenspace_of_forall_mapsTo, injOn_iInf_maxGenEigenspace, mem_iInf_maxGenEigenspace_iff, inf_iInf_maxGenEigenspace_of_forall_mapsTo	8
Total	8

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_iInf_maxGenEigenspace 📖	mathematical	—	Disjoint Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instPartialOrder Submodule.instOrderBot iInf Submodule.instInfSet maxGenEigenspace	—	Function.ne_iff Disjoint.mono iInf_le disjoint_genEigenspace
iInf_maxGenEigenspace_restrict_map_subtype_eq 📖	mathematical	Set.MapsTo DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe Submodule Submodule.setLike maxGenEigenspace	Submodule.map Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike maxGenEigenspace Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Submodule.subtype iInf Submodule.addCommGroup CommRing.toRing Submodule.instInfSet	—	le_antisymm iInf_le inf_le_right RingHomSurjective.ids Submodule.map_iInf Submodule.injective_subtype Submodule.inf_iInf Submodule.inf_genEigenspace
iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo 📖	mathematical	Set.MapsTo DFunLike.coe Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Submodule.setLike maxGenEigenspace iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Top.top Submodule.instTop	iSup Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice iInf Submodule.instInfSet maxGenEigenspace Top.top Submodule.instTop	—	forall_or_exists_not le_trans le_iSup Submodule.finrank_lt LT.lt.ne FiniteDimensional.finiteDimensional_submodule mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo genEigenspace_restrict_eq_top eq_bot_iff Submodule.ker_subtype LinearMap.ker.eq_1 RingHomSurjective.ids Submodule.map_le_iff_le_comap Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo disjoint_iff_inf_le Disjoint.mono_right iInf_le disjoint_genEigenspace instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors iSup_bot iSup_congr_Prop sup_of_le_right biSup_congr iSup_split iInf_maxGenEigenspace_restrict_map_subtype_eq Submodule.map.congr_simp Submodule.map_top Submodule.range_subtype iSup_comm iSup_iSup_eq_right
iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute 📖	mathematical	Pairwise Commute Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid instMul iSup Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice maxGenEigenspace Top.top Submodule.instTop	iSup Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice iInf Submodule.instInfSet maxGenEigenspace Top.top Submodule.instTop	—	iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo mapsTo_maxGenEigenspace_of_comm eq_or_ne
independent_iInf_maxGenEigenspace_of_forall_mapsTo 📖	mathematical	Set.MapsTo DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe Submodule Submodule.setLike maxGenEigenspace	iSupIndep Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice iInf Submodule.instInfSet maxGenEigenspace	—	Finset.induction_on Finset.sup_empty Finset.mem_insert Finset.sup_insert disjoint_iff Submodule.eq_bot_iff Submodule.mem_sup smulCommClass_self IsScalarTower.left mem_iInf_maxGenEigenspace_iff coe_pow Set.MapsTo.iterate Submodule.sub_mem Submodule.smul_mem Submodule.mem_inf Submodule.coe_iInf map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass zero_add RingHomSurjective.ids Submodule.map.congr_simp Finset.sup_eq_iSup Submodule.map_iSup iSup₂_mono Submodule.mem_map_of_mem Disjoint.eq_bot Submodule.mem_bot disjoint_iInf_maxGenEigenspace Submodule.instIsCompactlyGenerated Finset.notMem_erase
injOn_iInf_maxGenEigenspace 📖	mathematical	—	Set.InjOn Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid iInf Submodule.instInfSet maxGenEigenspace setOf Bot.bot Submodule.instBot	—	Mathlib.Tactic.Contrapose.contrapose₁ disjoint_iInf_maxGenEigenspace
mem_iInf_maxGenEigenspace_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike iInf Submodule.instInfSet maxGenEigenspace DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toPow instMonoid LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing instOne NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	smulCommClass_self

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf_iInf_maxGenEigenspace_of_forall_mapsTo 📖	mathematical	Set.MapsTo DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe Submodule setLike	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instMin iInf instInfSet Module.End.maxGenEigenspace map SetLike.instMembership setLike addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids subtype addCommGroup CommRing.toRing LinearMap.restrict	—	isEmpty_or_nonempty RingHomSurjective.ids iInf_of_isEmpty sInf_empty inf_of_le_left map.congr_simp map_top range_subtype inf_iInf inf_genEigenspace map_iInf injective_subtype

---

← Back to Index