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 SetLike.instMembership Submodule.addCommMonoid Submodule.module 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	iInf Submodule.instInfSet	—	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	iInf Submodule.instInfSet	—	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.completeLattice iInf Submodule.instInfSet	—	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 iSupIndep_iff_supIndep_of_injOn Submodule.instIsCompactlyGenerated injOn_iInf_maxGenEigenspace 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.toNatPow instMonoid LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid 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	instMin iInf instInfSet Module.End.maxGenEigenspace map SetLike.instMembership addCommMonoid module 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