LinearPMap

📁 Source: Mathlib/LinearAlgebra/LinearPMap.lean

Statistics

Metric	Count
Definitions `compPMap`, `toPMap`, `bot`, `codRestrict`, `comp`, `coprod`, `domRestrict`, `domain`, `eqLocus`, `fst`, `graph`, `inhabited`, `instAdd`, `instAddAction`, `instAddCommMonoid`, `instAddMonoid`, `instAddSemigroup`, `instAddZeroClass`, `instCoeFunForallSubtypeMemSubmoduleDomain`, `instInvolutiveNeg`, `instMulAction`, `instNeg`, `instSMul`, `instSub`, `instSubtractionCommMonoid`, `instVAdd`, `instZero`, `inverse`, `le`, `mkSpanSingleton`, `mkSpanSingleton'`, `orderBot`, `sSup`, `semilatticeInf`, `snd`, `sup`, `supSpanSingleton`, `toFun`, `toFun'`, `toLinearPMap`, `toLinearPMapAux`, `valFromGraph`, `[_]_»`	43
Theorems `compPMap_apply`, `toPMap_apply`, `toPMap_domain`, `add_apply`, `add_domain`, `apply_comp_inclusion`, `coe_smul`, `coe_vadd`, `coprod_apply`, `dExt`, `dExt_iff`, `domRestrict_apply`, `domRestrict_domain`, `domRestrict_le`, `domain_mkSpanSingleton`, `domain_mono`, `domain_sSup`, `domain_sup`, `domain_supSpanSingleton`, `eq_of_eq_graph`, `eq_of_le_of_domain_eq`, `exists_of_le`, `ext`, `ext'`, `ext_iff`, `fst_apply`, `graph_fst_eq_zero_snd`, `graph_map_fst_eq_domain`, `graph_map_snd_eq_range`, `image_iff`, `instIsScalarTower`, `instSMulCommClass`, `inverse_apply_eq`, `inverse_domain`, `inverse_graph`, `inverse_range`, `le_graph_iff`, `le_graph_of_le`, `le_of_eqLocus_ge`, `le_of_le_graph`, `le_sSup`, `left_le_sup`, `map_add`, `map_neg`, `map_smul`, `map_sub`, `map_zero`, `mem_domain_iff`, `mem_domain_iff_of_eq_graph`, `mem_domain_of_mem_graph`, `mem_domain_sSup_iff`, `mem_graph`, `mem_graph_iff`, `mem_graph_iff'`, `mem_graph_snd_inj`, `mem_graph_snd_inj'`, `mem_inverse_graph`, `mem_inverse_graph_snd_eq_zero`, `mem_range_iff`, `mkSpanSingleton'_apply`, `mkSpanSingleton'_apply_self`, `mkSpanSingleton_apply`, `mk_apply`, `neg_apply`, `neg_domain`, `neg_graph`, `right_le_sup`, `sSup_apply`, `sSup_le`, `smul_apply`, `smul_domain`, `smul_graph`, `snd_apply`, `sub_apply`, `sub_domain`, `supSpanSingleton_apply_mk`, `supSpanSingleton_apply_mk_of_mem`, `supSpanSingleton_apply_of_mem`, `supSpanSingleton_apply_self`, `supSpanSingleton_apply_smul_self`, `sup_apply`, `sup_h_of_disjoint`, `sup_le`, `toFun_eq_coe`, `vadd_apply`, `vadd_domain`, `zero_apply`, `zero_domain`, `existsUnique_from_graph`, `mem_graph_toLinearPMap`, `toLinearPMap_apply_aux`, `toLinearPMap_domain`, `toLinearPMap_graph_eq`, `toLinearPMap_range`, `valFromGraph_mem`	95
Total	138

LinearMap

Definitions

Name	Category	Theorems
`compPMap` 📖	CompOp	1 math math: `compPMap_apply`
`toPMap` 📖	CompOp	3 math math: `toPMap_apply`, `ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense`, `toPMap_domain`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compPMap_apply` 📖	mathematical	—	`LinearPMap.toFun'` `compPMap` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	—	—
`toPMap_apply` 📖	mathematical	—	`LinearPMap.toFun'` `toPMap` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `Submodule` `SetLike.instMembership` `Submodule.setLike`	—	—
`toPMap_domain` 📖	mathematical	—	`LinearPMap.domain` `toPMap`	—	—

LinearPMap

Definitions

Name	Category	Theorems
`bot` 📖	CompOp	—
`codRestrict` 📖	CompOp	—
`comp` 📖	CompOp	—
`coprod` 📖	CompOp	1 math math: `coprod_apply`
`domRestrict` 📖	CompOp	5 math math: `hasCore_def`, `HasCore.closure_eq`, `domRestrict_apply`, `domRestrict_domain`, `domRestrict_le`
`domain` 📖	CompOp	68 math math: `zero_domain`, `mem_domain_sSup_iff`, `HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk`, `closureHasCore`, `Submodule.toLinearPMap_range`, `sub_domain`, `HahnEmbedding.Partial.archimedeanClassMk_eq_iff`, `HahnEmbedding.Seed.baseEmbedding_strictMono`, `Module.Baer.ExtensionOf.is_extension`, `HahnEmbedding.Partial.toOrderAddMonoidHom_apply`, `smul_domain`, `HahnEmbedding.Partial.orderTop_eq_iff`, `HahnEmbedding.IsPartial.strictMono`, `HahnEmbedding.IsPartial.truncLT_mem_range`, `HasCore.le_domain`, `apply_comp_inclusion`, `sSup_apply`, `HahnEmbedding.Partial.truncLT_mem_range_sSupFun`, `sub_apply`, `IsSelfAdjoint.dense_domain`, `coe_smul`, `map_zero`, `map_add`, `domain_sSup`, `domain_mkSpanSingleton`, `adjointDomainMkCLM_apply`, `mem_domain_iff`, `LinearMap.toPMap_domain`, `add_apply`, `mem_graph_iff`, `map_neg`, `Submodule.toLinearPMap_domain`, `map_sub`, `map_smul`, `coprod_apply`, `domain_sup`, `Module.Baer.extensionOfMax_to_submodule_eq_top`, `HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk`, `mem_graph_iff'`, `HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding`, `HahnEmbedding.Partial.mem_domain`, `HahnEmbedding.Seed.mem_domain_baseEmbedding`, `mem_domain_of_mem_graph`, `mem_graph`, `neg_domain`, `mkSpanSingleton_apply`, `vadd_apply`, `ext_iff`, `Module.Baer.ExtensionOf.le`, `HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eq`, `mem_domain_iff_of_eq_graph`, `vadd_domain`, `domRestrict_domain`, `graph_map_fst_eq_domain`, `HahnEmbedding.Partial.sSupFun_strictMono`, `mem_adjoint_domain_iff`, `coe_vadd`, `HahnEmbedding.Partial.exists_domain_eq_top`, `exists_of_le`, `Module.Baer.ExtensionOfMaxAdjoin.eqn`, `add_domain`, `graph_map_snd_eq_range`, `domain_mono`, `HahnEmbedding.Seed.domain_baseEmbedding`, `toFun_eq_coe`, `mem_range_iff`, `inverse_domain`, `HahnEmbedding.Partial.toOrderAddMonoidHom_injective`
`eqLocus` 📖	CompOp	—
`fst` 📖	CompOp	1 math math: `fst_apply`
`graph` 📖	CompOp	21 math math: `inverse_graph`, `neg_graph`, `mem_inverse_graph`, `graph_adjoint_toLinearPMap_eq_adjoint`, `le_graph_iff`, `mem_domain_iff`, `mem_graph_iff`, `mem_graph_iff'`, `closure_def`, `mem_graph`, `smul_graph`, `le_graph_of_le`, `graph_map_fst_eq_domain`, `closure_inverse_graph`, `Submodule.toLinearPMap_graph_eq`, `graph_map_snd_eq_range`, `IsClosable.graph_closure_eq_closure_graph`, `mem_range_iff`, `adjoint_graph_eq_graph_adjoint`, `IsClosable.existsUnique`, `image_iff`
`inhabited` 📖	CompOp	—
`instAdd` 📖	CompOp	2 math math: `add_apply`, `add_domain`
`instAddAction` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	—
`instAddSemigroup` 📖	CompOp	—
`instAddZeroClass` 📖	CompOp	—
`instCoeFunForallSubtypeMemSubmoduleDomain` 📖	CompOp	—
`instInvolutiveNeg` 📖	CompOp	—
`instMulAction` 📖	CompOp	—
`instNeg` 📖	CompOp	3 math math: `neg_graph`, `neg_apply`, `neg_domain`
`instSMul` 📖	CompOp	6 math math: `instIsScalarTower`, `smul_domain`, `coe_smul`, `smul_graph`, `smul_apply`, `instSMulCommClass`
`instSub` 📖	CompOp	2 math math: `sub_domain`, `sub_apply`
`instSubtractionCommMonoid` 📖	CompOp	—
`instVAdd` 📖	CompOp	3 math math: `vadd_apply`, `vadd_domain`, `coe_vadd`
`instZero` 📖	CompOp	2 math math: `zero_domain`, `zero_apply`
`inverse` 📖	CompOp	8 math math: `inverse_graph`, `mem_inverse_graph`, `inverse_isClosable_iff`, `inverse_closure`, `inverse_range`, `inverse_closed_iff`, `closure_inverse_graph`, `inverse_domain`
`le` 📖	CompOp	14 math math: `HahnEmbedding.IsPartial.baseEmbedding_le`, `left_le_sup`, `Module.Baer.chain_linearPMap_of_chain_extensionOf`, `le_graph_iff`, `le_of_le_graph`, `RieszExtension.exists_top`, `IsFormalAdjoint.le_adjoint`, `right_le_sup`, `HahnEmbedding.Partial.baseEmbedding_le_extendFun`, `isClosable_iff_exists_closed_extension`, `le_closure`, `domRestrict_le`, `HahnEmbedding.Partial.exists_isMax`, `le_of_eqLocus_ge`
`mkSpanSingleton` 📖	CompOp	5 math math: `supSpanSingleton_apply_mk_of_mem`, `supSpanSingleton_apply_smul_self`, `supSpanSingleton_apply_self`, `mkSpanSingleton_apply`, `supSpanSingleton_apply_mk`
`mkSpanSingleton'` 📖	CompOp	1 math math: `domain_mkSpanSingleton`
`orderBot` 📖	CompOp	—
`sSup` 📖	CompOp	5 math math: `mem_domain_sSup_iff`, `sSup_apply`, `sSup_le`, `domain_sSup`, `le_sSup`
`semilatticeInf` 📖	CompOp	3 math math: `HahnEmbedding.Partial.lt_extend`, `RieszExtension.step`, `domain_mono`
`snd` 📖	CompOp	1 math math: `snd_apply`
`sup` 📖	CompOp	5 math math: `left_le_sup`, `sup_apply`, `sup_le`, `right_le_sup`, `domain_sup`
`supSpanSingleton` 📖	CompOp	5 math math: `domain_supSpanSingleton`, `supSpanSingleton_apply_mk_of_mem`, `supSpanSingleton_apply_smul_self`, `supSpanSingleton_apply_self`, `supSpanSingleton_apply_mk`
`toFun` 📖	CompOp	10 math math: `Submodule.toLinearPMap_range`, `HahnEmbedding.Partial.truncLT_mem_range_extendFun`, `HahnEmbedding.IsPartial.truncLT_mem_range`, `HahnEmbedding.Partial.truncLT_mem_range_sSupFun`, `HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding`, `mem_adjoint_domain_iff`, `HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun`, `graph_map_snd_eq_range`, `toFun_eq_coe`, `inverse_domain`
`toFun'` 📖	CompOp	73 math math: `HahnEmbedding.Seed.baseEmbedding_pos`, `Module.Baer.ExtensionOfMaxAdjoin.extensionToFun_wd`, `mk_apply`, `HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk`, `supSpanSingleton_apply_of_mem`, `neg_apply`, `LinearMap.compPMap_apply`, `mem_inverse_graph`, `HahnEmbedding.Partial.archimedeanClassMk_eq_iff`, `HahnEmbedding.Partial.truncLT_mem_range_extendFun`, `HahnEmbedding.Seed.baseEmbedding_strictMono`, `Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_eq`, `Module.Baer.ExtensionOf.is_extension`, `Module.Baer.ExtensionOf.dExt_iff`, `HahnEmbedding.Partial.toOrderAddMonoidHom_apply`, `HahnEmbedding.Partial.orderTop_eq_iff`, `HahnEmbedding.Partial.coeff_eq_of_mem`, `HahnEmbedding.Partial.extendFun_strictMono`, `LinearMap.toPMap_apply`, `HahnEmbedding.IsPartial.strictMono`, `supSpanSingleton_apply_mk_of_mem`, `HahnEmbedding.IsPartial.truncLT_mem_range`, `mkSpanSingleton'_apply_self`, `apply_comp_inclusion`, `sSup_apply`, `snd_apply`, `HahnEmbedding.Partial.truncLT_mem_range_sSupFun`, `sub_apply`, `domRestrict_apply`, `adjoint_apply_of_not_dense`, `coe_smul`, `map_zero`, `map_add`, `mkSpanSingleton'_apply`, `adjointDomainMkCLM_apply`, `HahnEmbedding.Seed.coeff_baseEmbedding`, `fst_apply`, `add_apply`, `mem_graph_iff`, `map_neg`, `map_sub`, `sup_h_of_disjoint`, `map_smul`, `dExt_iff`, `supSpanSingleton_apply_smul_self`, `coprod_apply`, `supSpanSingleton_apply_self`, `HahnEmbedding.Partial.coeff_eq_zero_of_mem`, `HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk`, `mem_graph_iff'`, `HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding`, `Submodule.toLinearPMap_apply_aux`, `HahnEmbedding.Partial.eval_lt`, `mem_graph`, `adjointDomainMkCLMExtend_apply`, `mkSpanSingleton_apply`, `vadd_apply`, `ext_iff`, `HahnEmbedding.Partial.eval_eq_truncLT`, `HahnEmbedding.Partial.evalCoeff_eq`, `HahnEmbedding.Partial.sSupFun_strictMono`, `smul_apply`, `coe_vadd`, `exists_of_le`, `supSpanSingleton_apply_mk`, `HahnEmbedding.Partial.apply_of_mem_stratum`, `adjointAux_inner`, `Submodule.mem_graph_toLinearPMap`, `adjoint_apply_of_dense`, `zero_apply`, `toFun_eq_coe`, `mem_range_iff`, `image_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`toFun'` `LinearPMap` `instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Submodule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.instMin` `Set` `Set.instMembership` `SetLike.coe` `Subtype.prop`	—	—
`add_domain` 📖	mathematical	—	`domain` `LinearPMap` `instAdd` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instMin`	—	—
`apply_comp_inclusion` 📖	mathematical	`LinearPMap` `le`	`toFun'` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `Submodule.inclusion` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	—
`coe_smul` 📖	mathematical	—	`toFun'` `LinearPMap` `instSMul` `Function.hasSMul` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`coe_vadd` 📖	mathematical	—	`toFun'` `HVAdd.hVAdd` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearPMap` `instHVAdd` `instVAdd` `Pi.instAdd` `Submodule` `SetLike.instMembership` `Submodule.setLike` `domain` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DFunLike.coe` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `LinearMap.comp` `RingHomCompTriple.ids` `Submodule.subtype`	—	—
`coprod_apply` 📖	mathematical	—	`toFun'` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `coprod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Submodule` `SetLike.instMembership` `Submodule.setLike` `domain` `Set` `Set.instMembership` `SetLike.coe`	—	—
`dExt` 📖	—	`domain` `toFun'`	—	—	`ext`
`dExt_iff` 📖	mathematical	—	`toFun'`	—	`dExt`
`domRestrict_apply` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `domain`	`toFun'` `domRestrict`	—	`mk_apply`
`domRestrict_domain` 📖	mathematical	—	`domain` `domRestrict` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instMin`	—	—
`domRestrict_le` 📖	mathematical	—	`LinearPMap` `le` `domRestrict`	—	`domRestrict_apply`
`domain_mkSpanSingleton` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`domain` `mkSpanSingleton'` `Submodule.span` `Set` `Set.instSingletonSet`	—	—
`domain_mono` 📖	mathematical	—	`StrictMono` `LinearPMap` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `semilatticeInf` `Submodule.instPartialOrder` `domain`	—	`lt_of_le_of_ne` `ne_of_lt` `eq_of_le_of_domain_eq` `le_of_lt`
`domain_sSup` 📖	mathematical	`DirectedOn` `LinearPMap` `le`	`domain` `sSup` `SupSet.sSup` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Set.image`	—	—
`domain_sup` 📖	mathematical	`toFun'`	`domain` `sup` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	—
`domain_supSpanSingleton` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain`	`supSpanSingleton` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.span` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Set` `Set.instSingletonSet`	—	—
`eq_of_eq_graph` 📖	—	`graph`	—	—	`dExt` `Submodule.ext` `mem_domain_iff_of_eq_graph` `le_of_le_graph` `Eq.le`
`eq_of_le_of_domain_eq` 📖	—	`LinearPMap` `le` `domain`	—	—	`dExt`
`exists_of_le` 📖	mathematical	`LinearPMap` `le`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `toFun'`	—	—
`ext` 📖	—	`domain` `toFun'` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike`	—	—	`LinearMap.ext`
`ext'` 📖	—	—	—	—	—
`ext_iff` 📖	mathematical	—	`domain` `toFun'` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike`	—	`ext`
`fst_apply` 📖	mathematical	—	`toFun'` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `fst` `Submodule` `Prod.instAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.prod`	—	—
`graph_fst_eq_zero_snd` 📖	—	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `Submodule.setLike` `graph` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`Submodule.zero_mem`
`graph_map_fst_eq_domain` 📖	mathematical	—	`Submodule.map` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.fst` `graph` `domain`	—	`Submodule.ext` `RingHomSurjective.ids`
`graph_map_snd_eq_range` 📖	mathematical	—	`Submodule.map` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.snd` `graph` `LinearMap.range` `Submodule` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.addCommMonoid` `Submodule.module` `toFun`	—	`Submodule.ext` `RingHomSurjective.ids`
`image_iff` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain`	`toFun'` `Prod.instAddCommMonoid` `Prod.instModule` `graph`	—	—
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `LinearPMap` `instSMul`	—	`ext'` `smul_assoc` `LinearMap.instIsScalarTower`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `LinearPMap` `instSMul`	—	`ext'` `SMulCommClass.smul_comm` `LinearMap.instSMulCommClass`
`inverse_apply_eq` 📖	—	`LinearMap.ker` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `toFun` `Bot.bot` `Submodule.instBot` `toFun'` `inverse`	—	—	`mem_inverse_graph`
`inverse_domain` 📖	mathematical	—	`domain` `inverse` `LinearMap.range` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `toFun`	—	`RingHomSurjective.ids` `inverse.eq_1` `Submodule.toLinearPMap_domain` `graph_map_snd_eq_range` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearEquiv.fst_comp_prodComm` `Submodule.map_comp`
`inverse_graph` 📖	mathematical	`LinearMap.ker` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `toFun` `Bot.bot` `Submodule.instBot`	`graph` `inverse` `Submodule.map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.prodComm`	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `inverse.eq_1` `Submodule.toLinearPMap_graph_eq` `mem_inverse_graph_snd_eq_zero`
`inverse_range` 📖	mathematical	`LinearMap.ker` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `toFun` `Bot.bot` `Submodule.instBot`	`LinearMap.range` `inverse` `RingHomSurjective.ids`	—	`RingHomSurjective.ids` `inverse.eq_1` `RingHomInvPair.ids` `Submodule.toLinearPMap_range` `mem_inverse_graph_snd_eq_zero` `graph_map_fst_eq_domain` `RingHomCompTriple.ids` `LinearEquiv.snd_comp_prodComm` `Submodule.map_comp`
`le_graph_iff` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `graph` `LinearPMap` `le`	—	`le_of_le_graph` `le_graph_of_le`
`le_graph_of_le` 📖	mathematical	`LinearPMap` `le`	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `graph`	—	`mem_graph_iff`
`le_of_eqLocus_ge` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `domain` `eqLocus`	`LinearPMap` `le`	—	`inf_le_left` `le_trans` `inf_le_right`
`le_of_le_graph` 📖	mathematical	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `graph`	`LinearPMap` `le`	—	`mem_domain_iff` `image_iff`
`le_sSup` 📖	mathematical	`DirectedOn` `LinearPMap` `le` `Set` `Set.instMembership`	`sSup`	—	—
`left_le_sup` 📖	mathematical	`toFun'`	`LinearPMap` `le` `sup`	—	`le_sup_left` `add_zero` `map_zero` `sup_apply`
`map_add` 📖	mathematical	—	`toFun'` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`LinearMap.map_add`
`map_neg` 📖	mathematical	—	`toFun'` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `NegMemClass.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubgroupClass.toNegMemClass` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Submodule.addSubgroupClass`	—	`LinearMap.map_neg`
`map_smul` 📖	mathematical	—	`toFun'` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid`	—	`LinearMap.map_smul`
`map_sub` 📖	mathematical	—	`toFun'` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `AddSubgroupClass.sub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Submodule.addSubgroupClass` `SubNegMonoid.toSub`	—	`LinearMap.map_sub`
`map_zero` 📖	mathematical	—	`toFun'` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`LinearMap.map_zero`
`mem_domain_iff` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Prod.instAddCommMonoid` `Prod.instModule` `graph`	—	`mem_graph`
`mem_domain_iff_of_eq_graph` 📖	mathematical	`graph`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain`	—	—
`mem_domain_of_mem_graph` 📖	mathematical	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `Submodule.setLike` `graph`	`domain`	—	`mem_domain_iff`
`mem_domain_sSup_iff` 📖	mathematical	`Set.Nonempty` `LinearPMap` `DirectedOn` `le`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `sSup` `Set` `Set.instMembership`	—	`domain_sSup` `Submodule.mem_sSup_of_directed` `Set.Nonempty.image` `DirectedOn.mono_comp` `StrictMono.monotone` `domain_mono`
`mem_graph` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `Submodule.setLike` `graph` `domain` `toFun'`	—	—
`mem_graph_iff` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `Submodule.setLike` `graph` `domain` `toFun'`	—	—
`mem_graph_iff'` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `Submodule.setLike` `graph` `domain` `toFun'`	—	—
`mem_graph_snd_inj` 📖	—	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `Submodule.setLike` `graph`	—	—	—
`mem_graph_snd_inj'` 📖	—	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `Submodule.setLike` `graph`	—	—	—
`mem_inverse_graph` 📖	mathematical	`LinearMap.ker` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `toFun` `Bot.bot` `Submodule.instBot`	`Prod.instAddCommMonoid` `Prod.instModule` `graph` `inverse` `toFun'`	—	`RingHomInvPair.ids` `RingHomSurjective.ids` `inverse_graph`
`mem_inverse_graph_snd_eq_zero` 📖	—	`LinearMap.ker` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `toFun` `Bot.bot` `Submodule.instBot` `Prod.instAddCommMonoid` `Prod.instModule` `Submodule.map` `RingHomSurjective.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.prodComm` `graph` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `Submodule.map_equiv_eq_comap_symm` `LinearMap.ker_eq_bot'`
`mem_range_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `toFun'` `Prod.instAddCommMonoid` `Prod.instModule` `graph`	—	`Set.mem_range` `mem_graph`
`mkSpanSingleton'_apply` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `domain` `mkSpanSingleton'`	`toFun'`	—	`sub_eq_zero` `sub_smul` `Submodule.mem_span_singleton`
`mkSpanSingleton'_apply_self` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `domain` `mkSpanSingleton'`	`toFun'`	—	`one_smul` `mkSpanSingleton'_apply`
`mkSpanSingleton_apply` 📖	mathematical	—	`toFun'` `DivisionRing.toRing` `mkSpanSingleton` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.mem_span_singleton_self` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring`	—	`mkSpanSingleton'_apply_self` `Submodule.mem_span_singleton_self`
`mk_apply` 📖	mathematical	—	`toFun'` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike`	—	—
`neg_apply` 📖	mathematical	—	`toFun'` `LinearPMap` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`neg_domain` 📖	mathematical	—	`domain` `LinearPMap` `instNeg`	—	—
`neg_graph` 📖	mathematical	—	`graph` `LinearPMap` `instNeg` `Submodule.map` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.prodMap` `LinearMap.id` `LinearMap` `LinearMap.instNeg`	—	`Submodule.ext` `RingHomSurjective.ids` `mem_graph_iff` `Submodule.mem_map` `neg_apply`
`right_le_sup` 📖	mathematical	`toFun'`	`LinearPMap` `le` `sup`	—	`le_sup_right` `zero_add` `map_zero` `sup_apply`
`sSup_apply` 📖	mathematical	`DirectedOn` `LinearPMap` `le` `Set` `Set.instMembership`	`toFun'` `sSup` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `le_sSup`	—	`le_sSup`
`sSup_le` 📖	mathematical	`DirectedOn` `LinearPMap` `le`	`sSup`	—	`le_of_eqLocus_ge` `sSup_le` `le_inf` `le_sSup`
`smul_apply` 📖	mathematical	—	`toFun'` `LinearPMap` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`smul_domain` 📖	mathematical	—	`domain` `LinearPMap` `instSMul`	—	—
`smul_graph` 📖	mathematical	—	`graph` `LinearPMap` `instSMul` `Submodule.map` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.prodMap` `LinearMap.id` `LinearMap` `LinearMap.instSMul` `DistribMulAction.toDistribSMul` `AddCommMonoid.toAddMonoid`	—	`Submodule.ext` `RingHomSurjective.ids` `mem_graph_iff` `Submodule.mem_map` `smul_apply`
`snd_apply` 📖	mathematical	—	`toFun'` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `snd` `Submodule` `Prod.instAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.prod`	—	—
`sub_apply` 📖	mathematical	—	`toFun'` `LinearPMap` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.instMin` `Set` `Set.instMembership` `SetLike.coe` `Subtype.prop`	—	—
`sub_domain` 📖	mathematical	—	`domain` `LinearPMap` `instSub` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instMin`	—	—
`supSpanSingleton_apply_mk` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain`	`toFun'` `supSpanSingleton` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `mkSpanSingleton` `Submodule.mem_sup` `AddCommMonoid.toAddMonoid` `Submodule.span` `Set` `Set.instSingletonSet` `Submodule.mem_span_singleton`	—	`Submodule.mem_sup` `Submodule.mem_span_singleton` `sup_apply` `mkSpanSingleton'_apply`
`supSpanSingleton_apply_mk_of_mem` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain`	`toFun'` `supSpanSingleton` `Submodule.mem_sup_left` `mkSpanSingleton`	—	`supSpanSingleton_apply_of_mem` `Submodule.mem_sup_left`
`supSpanSingleton_apply_of_mem` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `supSpanSingleton`	`toFun'`	—	`Submodule.mem_sup` `Submodule.mem_span_singleton` `zero_smul` `add_zero` `Subtype.coe_eta`
`supSpanSingleton_apply_self` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain`	`toFun'` `supSpanSingleton` `Submodule.mem_sup_right` `mkSpanSingleton` `Submodule.mem_span_singleton_self`	—	`Submodule.mem_sup_right` `Submodule.mem_span_singleton_self` `Submodule.mem_span_singleton` `one_smul` `supSpanSingleton_apply_smul_self`
`supSpanSingleton_apply_smul_self` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain`	`toFun'` `supSpanSingleton` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `Submodule.mem_sup_right` `mkSpanSingleton` `Submodule.span` `Set` `Set.instSingletonSet` `AddCommMonoid.toAddMonoid` `Submodule.mem_span_singleton`	—	`Submodule.mem_sup_right` `Submodule.mem_span_singleton` `Submodule.mem_sup` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `zero_add` `Submodule.mk_eq_zero` `map_zero`
`sup_apply` 📖	mathematical	`toFun'` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Submodule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `domain` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	`sup`	—	—
`sup_h_of_disjoint` 📖	mathematical	`Disjoint` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `Submodule.instOrderBot` `domain` `SetLike.instMembership` `Submodule.setLike`	`toFun'`	—	`Submodule.disjoint_def` `map_zero`
`sup_le` 📖	mathematical	`toFun'` `LinearPMap` `le`	`sup`	—	`le_inf` `left_le_sup` `right_le_sup` `le_of_eqLocus_ge` `sup_le`
`toFun_eq_coe` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `domain` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `toFun` `toFun'`	—	—
`vadd_apply` 📖	mathematical	—	`toFun'` `HVAdd.hVAdd` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearPMap` `instHVAdd` `instVAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DFunLike.coe` `LinearMap.instFunLike` `Submodule` `SetLike.instMembership` `Submodule.setLike` `domain`	—	—
`vadd_domain` 📖	mathematical	—	`domain` `HVAdd.hVAdd` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearPMap` `instHVAdd` `instVAdd`	—	—
`zero_apply` 📖	mathematical	—	`toFun'` `LinearPMap` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`zero_domain` 📖	mathematical	—	`domain` `LinearPMap` `instZero` `Top.top` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instTop`	—	—

Submodule

Definitions

Name	Category	Theorems
`toLinearPMap` 📖	CompOp	6 math math: `toLinearPMap_range`, `LinearPMap.graph_adjoint_toLinearPMap_eq_adjoint`, `toLinearPMap_domain`, `toLinearPMap_apply_aux`, `toLinearPMap_graph_eq`, `mem_graph_toLinearPMap`
`toLinearPMapAux` 📖	CompOp	—
`valFromGraph` 📖	CompOp	2 math math: `toLinearPMap_apply_aux`, `valFromGraph_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`existsUnique_from_graph` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.fst`	`ExistsUnique`	—	`RingHomSurjective.ids` `existsUnique_of_exists_of_unique` `sub_self` `sub_mem` `sub_eq_zero`
`mem_graph_toLinearPMap` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `setLike` `map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.fst` `LinearPMap.toFun'` `toLinearPMap`	—	`RingHomSurjective.ids` `toLinearPMap_apply_aux` `valFromGraph_mem`
`toLinearPMap_apply_aux` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`LinearPMap.toFun'` `toLinearPMap` `valFromGraph` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.fst`	—	`RingHomSurjective.ids`
`toLinearPMap_domain` 📖	mathematical	—	`LinearPMap.domain` `toLinearPMap` `map` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.fst`	—	—
`toLinearPMap_graph_eq` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`LinearPMap.graph` `toLinearPMap`	—	`ext` `LinearPMap.mem_graph_iff` `RingHomSurjective.ids` `mem_graph_toLinearPMap` `toLinearPMap_apply_aux` `ExistsUnique.unique` `existsUnique_from_graph` `valFromGraph_mem`
`toLinearPMap_range` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`LinearMap.range` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `LinearPMap.domain` `toLinearPMap` `addCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearPMap.toFun` `map` `Prod.instAddCommMonoid` `Prod.instModule` `LinearMap.snd`	—	`RingHomSurjective.ids` `LinearPMap.graph_map_snd_eq_range` `toLinearPMap_graph_eq`
`valFromGraph_mem` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.fst`	`valFromGraph`	—	`RingHomSurjective.ids` `ExistsUnique.exists` `existsUnique_from_graph`

(root)

Definitions

Name	Category	Theorems
`«term_→ₗ.[_]_»` 📖	CompOp	—

---

← Back to Index