Documentation Verification Report

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	42 math math: `mem_invtSubmodule`, `RootPairing.Base.forall_mem_support_invtSubmodule_iff`, `LinearMap.IsProj.mem_invtSubmodule_iff`, `LinearMap.IsIdempotentElem.commute_iff`, `LinearEquiv.map_mem_invtSubmodule_conj_iff`, `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`, `VonNeumannAlgebra.IsIdempotentElem.mem_iff`, `VonNeumannAlgebra.IsStarProjection.mem_iff`, `LinearMap.IsIdempotentElem.range_mem_invtSubmodule`, `Module.AEval.mem_mapSubmodule_symm_apply`, `mem_invtSubmodule_symm_iff_le_map`, `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`, `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.bot_mem`, `mem_invtSubmodule_iff_map_le`, `Module.AEval.mem_mapSubmodule_apply`, `Representation.mem_invtSubmodule`, `Submodule.mem_invtSubmodule_reflection_iff`, `invtSubmodule.disjoint_iff`, `isSemisimple_iff`, `ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff`

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` `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`	`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` `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`
`inf_mem` 📖	mathematical	`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` `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.map` `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`	`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`	`Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `BoundedOrder.toOrderTop` `instBoundedOrderSubtypeSubmoduleMemSublattice` `Submodule.instTop`	—	`Subtype.mk_eq_top_iff`
`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`	`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`	—	—
`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`	`Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Module.End.invtSubmodule`	—	`Module.End.mem_invtSubmodule_iff_mapsTo`

---

← Back to Index