Invariant

📁 Source: Mathlib/Algebra/Module/Submodule/Invariant.lean

Statistics

Metric	Count
Definitions invtSubmodule, instBoundedOrderSubtypeSubmoduleMemSublattice	2
Theorems map_mem_invtSubmodule_conj_iff, map_mem_invtSubmodule_iff, bot_mem, codisjoint_iff, codisjoint_mk_iff, comp, disjoint_iff, disjoint_mk_iff, id, inf_mem, isCompl_iff, isCompl_mk_iff, map_subtype_mem_of_mem_invtSubmodule, mk_eq_bot_iff, mk_eq_top_iff, one, sup_mem, top_mem, zero, mem_invtSubmodule, mem_invtSubmodule_iff_forall_mem_of_mem, mem_invtSubmodule_iff_map_le, mem_invtSubmodule_iff_mapsTo, mem_invtSubmodule_symm_iff_le_map, span_orbit_mem_invtSubmodule, mem_invtSubmodule	26
Total	28

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mem_invtSubmodule_conj_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.End LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike conj Submodule.map RingHomSurjective.ids toLinearMap	—	RingHomInvPair.ids RingHomCompTriple.ids LinearMap.ext symm_apply_apply smulCommClass_self RingHomSurjective.ids RingHomInvPair.triples₂ conj_apply Module.End.mem_invtSubmodule Submodule.map_le_iff_le_comap RingHomSurjective.invPair Submodule.map_equiv_eq_comap_symm Submodule.comap_comp
map_mem_invtSubmodule_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids toLinearMap RingHomInvPair.ids DFunLike.coe LinearEquiv Module.End LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike instEquivLike conj symm	—	RingHomInvPair.ids RingHomSurjective.ids smulCommClass_self map_mem_invtSubmodule_conj_iff conj_conj_symm

Module.End

Definitions

Name	Category	Theorems
invtSubmodule 📖	CompOp	61 math math: isSemisimple_restrict_iff, mem_invtSubmodule, RootPairing.Base.forall_mem_support_invtSubmodule_iff, LinearMap.IsProj.mem_invtSubmodule_iff, LinearMap.IsIdempotentElem.commute_iff, invtSubmodule.disjoint_mk_iff, LinearEquiv.map_mem_invtSubmodule_conj_iff, genEigenspace_mem_invtSubmodule, Submodule.mem_invtSubmodule_reflection_of_mem, mem_invtSubmodule_iff_mapsTo, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule, RootPairing.mem_invtRootSubmodule_iff, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, invtSubmodule.isCompl_iff, invtSubmodule.one, RootPairing.corootSpan_mem_invtSubmodule_coreflection, isFinitelySemisimple_iff, restrict_eigenspace, invtSubmodule.sup_mem, VonNeumannAlgebra.IsIdempotentElem.mem_iff, invtSubmodule.mk_eq_top_iff, invtSubmodule.inf_mem, invtSubmodule.map_subtype_mem_of_mem_invtSubmodule, VonNeumannAlgebra.IsStarProjection.mem_iff, Submodule.topologicalClosure_mem_invtSubmodule, LinearMap.IsIdempotentElem.range_mem_invtSubmodule, Module.AEval.mem_mapSubmodule_symm_apply, mem_invtSubmodule_symm_iff_le_map, invtSubmodule.isCompl_mk_iff, span_orbit_mem_invtSubmodule, invtSubmodule.codisjoint_iff, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, ContinuousLinearMap.IsIdempotentElem.commute_iff, Set.Mapsto.mem_invtSubmodule, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule, mem_invtSubmodule_iff_forall_mem_of_mem, invtSubmodule.top_mem, eigenspace_mem_invtSubmodule, mem_invtSubmodule_adjoint_iff, RootPairing.rootSpan_mem_invtSubmodule_reflection, isSemisimple_iff', LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, invtSubmodule.zero, invtSubmodule.id, LinearEquiv.map_mem_invtSubmodule_iff, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule, invtSubmodule.mk_eq_bot_iff, invtSubmodule.comp, RootPairing.invtSubmodule_reflection_of_invtSubmodule_coreflection, invtSubmodule.bot_mem, ContinuousLinearMap.orthogonal_mem_invtSubmodule, mem_invtSubmodule_iff_map_le, invtSubmodule.codisjoint_mk_iff, Module.AEval.mem_mapSubmodule_apply, Representation.mem_invtSubmodule, Submodule.mem_invtSubmodule_reflection_iff, invtSubmodule.disjoint_iff, isSemisimple_iff, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, ContinuousLinearMap.mem_invtSubmodule_adjoint_iff, LinearMap.IsSymmetric.orthogonalComplement_mem_invtSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_invtSubmodule 📖	mathematical	—	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike invtSubmodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.comap RingHom.id Semiring.toNonAssocSemiring	—	—
mem_invtSubmodule_iff_forall_mem_of_mem 📖	mathematical	—	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike invtSubmodule Submodule.setLike DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring	—	—
mem_invtSubmodule_iff_map_le 📖	mathematical	—	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike invtSubmodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids	—	RingHomSurjective.ids Submodule.map_le_iff_le_comap
mem_invtSubmodule_iff_mapsTo 📖	mathematical	—	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike invtSubmodule Set.MapsTo DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe Submodule.setLike	—	—
mem_invtSubmodule_symm_iff_le_map 📖	mathematical	—	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike invtSubmodule LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearEquiv.symm Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.map RingHomSurjective.ids	—	RingHomInvPair.ids RingHomSurjective.ids mem_invtSubmodule_iff_map_le Equiv.subset_symm_image
span_orbit_mem_invtSubmodule 📖	mathematical	—	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike invtSubmodule DistribSMul.toLinearMap DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid Submodule.span MulAction.orbit SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass	—	mem_invtSubmodule Submodule.span_le Submodule.comap_coe Submodule.subset_span MulAction.mem_orbit_of_mem_orbit

Module.End.invtSubmodule

Definitions

Name	Category	Theorems
instBoundedOrderSubtypeSubmoduleMemSublattice 📖	CompOp	9 math math: disjoint_mk_iff, isCompl_iff, mk_eq_top_iff, isCompl_mk_iff, codisjoint_iff, Module.End.isSemisimple_iff', mk_eq_bot_iff, codisjoint_mk_iff, disjoint_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_mem 📖	mathematical	—	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Bot.bot Submodule.instBot	—	—
codisjoint_iff 📖	mathematical	—	Codisjoint Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Subtype.partialOrder Submodule.instPartialOrder BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder instBoundedOrderSubtypeSubmoduleMemSublattice Submodule.instOrderTop	—	—
codisjoint_mk_iff 📖	mathematical	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule	Codisjoint Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Subtype.partialOrder Submodule.instPartialOrder BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder instBoundedOrderSubtypeSubmoduleMemSublattice Submodule.instOrderTop	—	codisjoint_iff Sublattice.supClosed Subtype.mk_eq_top_iff
comp 📖	mathematical	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
disjoint_iff 📖	mathematical	—	Disjoint Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Subtype.partialOrder Submodule.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder instBoundedOrderSubtypeSubmoduleMemSublattice Submodule.instOrderBot	—	—
disjoint_mk_iff 📖	mathematical	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule	Disjoint Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Subtype.partialOrder Submodule.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder instBoundedOrderSubtypeSubmoduleMemSublattice Submodule.instOrderBot	—	disjoint_iff Sublattice.infClosed Subtype.mk_eq_bot_iff
id 📖	mathematical	—	Module.End.invtSubmodule LinearMap.id Top.top Sublattice Submodule ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instTop	—	eq_top_iff Submodule.comap_id instReflLe
inf_mem 📖	mathematical	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Submodule.instMin	—	Sublattice.inf_mem
isCompl_iff 📖	mathematical	—	IsCompl Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Subtype.partialOrder Submodule.instPartialOrder instBoundedOrderSubtypeSubmoduleMemSublattice CompleteLattice.toBoundedOrder	—	—
isCompl_mk_iff 📖	mathematical	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule	IsCompl Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Subtype.partialOrder Submodule.instPartialOrder instBoundedOrderSubtypeSubmoduleMemSublattice CompleteLattice.toBoundedOrder	—	—
map_subtype_mem_of_mem_invtSubmodule 📖	mathematical	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Submodule.setLike Submodule.addCommMonoid Submodule.module LinearMap.restrict	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Submodule.map Submodule.setLike Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Submodule.subtype	—	RingHomSurjective.ids LinearMap.restrict_apply Submodule.mem_comap
mk_eq_bot_iff 📖	mathematical	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder BoundedOrder.toOrderBot instBoundedOrderSubtypeSubmoduleMemSublattice Submodule.instBot	—	Subtype.mk_eq_bot_iff
mk_eq_top_iff 📖	mathematical	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder BoundedOrder.toOrderTop instBoundedOrderSubtypeSubmoduleMemSublattice Submodule.instTop	—	Subtype.mk_eq_top_iff instReflLe
one 📖	mathematical	—	Module.End.invtSubmodule Module.End Module.End.instOne Top.top Sublattice Submodule ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instTop	—	id
sup_mem 📖	mathematical	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Sublattice.sup_mem
top_mem 📖	mathematical	—	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule Top.top Submodule.instTop	—	instReflLe
zero 📖	mathematical	—	Module.End.invtSubmodule Module.End LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring Top.top Sublattice Submodule ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instTop	—	eq_top_iff Submodule.comap_zero

Set.Mapsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_invtSubmodule 📖	mathematical	Set.MapsTo DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe Submodule Submodule.setLike	Submodule Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule	—	Module.End.mem_invtSubmodule_iff_mapsTo

---

← Back to Index