Documentation Verification Report

EqLocus

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

Statistics

Metric	Count
Definitions `eqLocus`	1
Theorems `eqLocus_eq_ker_sub`, `eqLocus_eq_top`, `eqLocus_same`, `eqLocus_toAddSubmonoid`, `eqOn_sup`, `ext_on_codisjoint`, `le_eqLocus`, `mem_eqLocus`	8
Total	9

LinearMap

Definitions

Name	Category	Theorems
`eqLocus` 📖	CompOp	14 math math: `eqLocus_same`, `ContinuousLinearMap.completeSpace_eqLocus`, `tensorEqLocusEquiv_apply`, `tensorEqLocus_coe`, `mem_eqLocus`, `Module.Flat.eqLocus_lTensor_eq`, `eqLocus_toAddSubmonoid`, `tensorEqLocus_tmul`, `eqLocus_eq_top`, `eqLocus_eq_ker_sub`, `le_eqLocus`, `ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection`, `AlgHom.equalizer_toSubmodule`, `lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eqLocus_eq_ker_sub` 📖	mathematical	—	`eqLocus` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap` `instFunLike` `semilinearMapClass` `ker` `instSub`	—	`SetLike.ext` `semilinearMapClass` `sub_eq_zero`
`eqLocus_eq_top` 📖	mathematical	—	`eqLocus` `Top.top` `Submodule` `Submodule.instTop`	—	—
`eqLocus_same` 📖	mathematical	—	`eqLocus` `Top.top` `Submodule` `Submodule.instTop`	—	`eqLocus_eq_top`
`eqLocus_toAddSubmonoid` 📖	mathematical	—	`Submodule.toAddSubmonoid` `eqLocus` `AddMonoidHom.eqLocusM` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHomClass.toAddMonoidHom` `AddZeroClass.toAddZero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SemilinearMapClass.distribMulActionSemiHomClass`	—	—
`eqOn_sup` 📖	mathematical	`Set.EqOn` `DFunLike.coe` `SetLike.coe` `Submodule` `Submodule.setLike`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`le_eqLocus` `sup_le`
`ext_on_codisjoint` 📖	—	`Codisjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderTop` `Set.EqOn` `DFunLike.coe` `SetLike.coe` `Submodule.setLike`	—	—	`DFunLike.ext` `eqOn_sup` `Codisjoint.eq_top`
`le_eqLocus` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `eqLocus` `Set.EqOn` `DFunLike.coe` `SetLike.coe` `Submodule.setLike`	—	—
`mem_eqLocus` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `eqLocus` `DFunLike.coe`	—	—

---

← Back to Index