Documentation Verification Report

MStructure

📁 Source: Mathlib/Analysis/Normed/Module/MStructure.lean

Statistics

Metric	Count
Definitions `IsLprojection`, `boundedOrder`, `distribLattice`, `inf`, `instCompl`, `one`, `partialOrder`, `sdiff`, `sup`, `zero`, `instLatticeSubtypeOfFaithfulSMul`, `IsMprojection`	12
Theorems `Lcomplement`, `Lcomplement_iff`, `Lnorm`, `coe_bot`, `coe_compl`, `coe_inf`, `coe_one`, `coe_sdiff`, `coe_sup`, `coe_top`, `coe_zero`, `commute`, `compl_mul`, `distrib_lattice_lemma`, `join`, `le_def`, `mul`, `mul_compl_self`, `proj`, `Mnorm`, `proj`	21
Total	33

IsLprojection

Definitions

Name	Category	Theorems
`instLatticeSubtypeOfFaithfulSMul` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Lcomplement` 📖	mathematical	`IsLprojection`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`IsIdempotentElem.one_sub` `proj` `add_comm` `sub_sub_cancel` `Lnorm`
`Lcomplement_iff` 📖	mathematical	—	`IsLprojection` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Lcomplement` `sub_sub_cancel`
`Lnorm` 📖	mathematical	`IsLprojection`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real` `Real.instAdd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SubNegMonoid.toSub` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—
`coe_bot` 📖	mathematical	—	`IsLprojection` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `Subtype.partialOrder` `BoundedOrder.toOrderBot` `Subtype.boundedOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`coe_compl` 📖	mathematical	—	`IsLprojection` `Compl.compl` `Subtype.instCompl` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—
`coe_inf` 📖	mathematical	—	`IsLprojection` `Subtype.inf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`coe_one` 📖	mathematical	—	`IsLprojection` `Subtype.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`coe_sdiff` 📖	mathematical	—	`IsLprojection` `Subtype.sdiff` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—
`coe_sup` 📖	mathematical	—	`IsLprojection` `Subtype.sup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul`	—	—
`coe_top` 📖	mathematical	—	`IsLprojection` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `Subtype.partialOrder` `BoundedOrder.toOrderTop` `Subtype.boundedOrder` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`coe_zero` 📖	mathematical	—	`IsLprojection` `Subtype.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`commute` 📖	mathematical	`IsLprojection`	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`FaithfulSMul.eq_of_smul_eq_smul` `norm_sub_eq_zero_iff` `Lnorm` `sub_smul` `one_smul` `smul_sub` `SemigroupAction.mul_smul` `IsIdempotentElem.eq` `proj` `sub_mul` `one_mul` `sub_self` `zero_smul` `zero_sub` `norm_neg` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.subst_into_smul_upcast` `Mathlib.Tactic.Abel.term_smulg` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Abel.zero_smulg` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `norm_le_insert'` `le_antisymm_iff` `Nat.instAtLeastTwoHAddOfNat` `mul_le_mul_iff_right₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instNontrivial` `MulZeroClass.mul_zero` `two_mul` `two_smul` `add_le_add_iff_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `norm_nonneg` `Lcomplement` `sub_eq_add_neg` `add_mul` `Distrib.rightDistribClass` `neg_mul` `mul_add` `Distrib.leftDistribClass` `mul_one` `mul_neg` `mul_assoc` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `sub_eq_zero` `add_eq_left` `eq_sub_iff_add_eq`
`compl_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsLprojection` `Compl.compl` `Subtype.instCompl` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`coe_compl` `sub_mul` `one_mul`
`distrib_lattice_lemma` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `IsLprojection` `Compl.compl` `Subtype.instCompl`	—	`add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `mul_assoc` `coe_inf` `Commute.eq` `commute` `Subtype.prop` `mul_compl_self` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `zero_add` `add_zero` `IsIdempotentElem.eq` `proj`
`join` 📖	mathematical	`IsLprojection`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul`	—	`sub_eq_add_neg` `mul_add` `Distrib.leftDistribClass` `mul_one` `mul_neg` `add_mul` `Distrib.rightDistribClass` `one_mul` `neg_mul` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Abel.zero_termg` `Lcomplement_iff` `mul` `Lcomplement`
`le_def` 📖	mathematical	—	`IsLprojection` `Preorder.toLE` `PartialOrder.toPreorder` `Subtype.partialOrder` `Subtype.inf`	—	—
`mul` 📖	mathematical	`IsLprojection`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`IsIdempotentElem.mul_of_commute` `commute` `proj` `le_antisymm` `add_sub_cancel` `norm_add_le` `sub_smul` `one_smul` `Lnorm` `add_assoc` `add_le_add_iff_left` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `sub_add_sub_cancel'` `SemigroupAction.mul_smul`
`mul_compl_self` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsLprojection` `Compl.compl` `Subtype.instCompl` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`coe_compl` `IsIdempotentElem.mul_one_sub_self` `proj` `Subtype.prop`
`proj` 📖	mathematical	`IsLprojection`	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—

IsLprojection.Subtype

Definitions

Name	Category	Theorems
`boundedOrder` 📖	CompOp	2 math math: `IsLprojection.coe_top`, `IsLprojection.coe_bot`
`distribLattice` 📖	CompOp	—
`inf` 📖	CompOp	2 math math: `IsLprojection.coe_inf`, `IsLprojection.le_def`
`instCompl` 📖	CompOp	4 math math: `IsLprojection.coe_compl`, `IsLprojection.distrib_lattice_lemma`, `IsLprojection.mul_compl_self`, `IsLprojection.compl_mul`
`one` 📖	CompOp	1 math math: `IsLprojection.coe_one`
`partialOrder` 📖	CompOp	3 math math: `IsLprojection.coe_top`, `IsLprojection.coe_bot`, `IsLprojection.le_def`
`sdiff` 📖	CompOp	1 math math: `IsLprojection.coe_sdiff`
`sup` 📖	CompOp	1 math math: `IsLprojection.coe_sup`
`zero` 📖	CompOp	1 math math: `IsLprojection.coe_zero`

IsMprojection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Mnorm` 📖	mathematical	`IsMprojection`	`Norm.norm` `NormedAddCommGroup.toNorm` `Real` `Real.instMax` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SubNegMonoid.toSub` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	—
`proj` 📖	mathematical	`IsMprojection`	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—

(root)

Definitions

Name	Category	Theorems
`IsLprojection` 📖	CompData	13 math math: `IsLprojection.coe_zero`, `IsLprojection.coe_compl`, `IsLprojection.coe_top`, `IsLprojection.coe_bot`, `IsLprojection.coe_one`, `IsLprojection.coe_sdiff`, `IsLprojection.Lcomplement_iff`, `IsLprojection.distrib_lattice_lemma`, `IsLprojection.mul_compl_self`, `IsLprojection.coe_sup`, `IsLprojection.coe_inf`, `IsLprojection.compl_mul`, `IsLprojection.le_def`
`IsMprojection` 📖	CompData	—

---

← Back to Index