RestrictScalars

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

Statistics

Metric	Count
Definitions `restrictScalars`, `origModule`, `restrictScalarsEmbedding`, `restrictScalarsEquiv`, `restrictScalarsLatticeHom`	5
Theorems `coe_restrictScalars`, `isScalarTower`, `restrictScalarsEmbedding_apply`, `restrictScalarsEquiv_apply`, `restrictScalarsEquiv_symm_apply`, `restrictScalars_bot`, `restrictScalars_eq_bot_iff`, `restrictScalars_eq_top_iff`, `restrictScalars_iInf`, `restrictScalars_iSup`, `restrictScalars_inf`, `restrictScalars_inj`, `restrictScalars_injective`, `restrictScalars_le`, `restrictScalars_lt`, `restrictScalars_mem`, `restrictScalars_mono`, `restrictScalars_monotone`, `restrictScalars_sInf`, `restrictScalars_sSup`, `restrictScalars_self`, `restrictScalars_sup`, `restrictScalars_top`, `toAddSubmonoid_restrictScalars`, `toIntSubmodule_toAddSubgroup`	25
Total	30

Submodule

Definitions

Name	Category	Theorems
`restrictScalars` 📖	CompOp	79 math math: `Algebra.idealMap_eq_ofEq_comp_toLocalized₀`, `Ideal.finrank_eq_finrank`, `Ideal.smul_top_eq_map`, `Algebra.Extension.H1Cotangent.equiv_apply`, `FG.restrictScalars_of_surjective`, `restrictScalars_eq_bot_iff`, `restrictScalars_monotone`, `restrictScalars_mul`, `restrictScalars_bot`, `Ideal.range_cotangentToQuotientSquare`, `LinearMap.ker_localizedMap_eq_localized'_ker`, `restrictScalars_top`, `LinearMap.ker_restrictScalars`, `span_range_inclusion_restrictScalars_eq_top`, `FG.restrictScalars`, `element_smul_restrictScalars`, `Ideal.range_mul`, `traceDual_top'`, `Ideal.map_includeRight_eq`, `span_le_restrictScalars`, `restrictScalars_lt`, `le_spanRank_restrictScalars`, `FG.restrictScalars_iff`, `differentialIdeal_le_iff`, `restrictScalars_le`, `coe_restrictScalars`, `spanRank_restrictScalars_eq`, `fg_restrictScalars`, `KaehlerDifferential.ker_map`, `toIntSubmodule_toAddSubgroup`, `traceDual_le_span_map_traceDual`, `restrictScalars_sSup`, `restrictScalarsEquiv_symm_apply`, `Ideal.coe_restrictScalars`, `Quotient.restrictScalarsEquiv_symm_mk`, `restrictScalars_traceDual`, `differentialIdeal_le_fractionalIdeal_iff`, `Ideal.localized₀_eq_restrictScalars_map`, `KaehlerDifferential.kerTotal_map`, `restrictScalars_mono`, `derivationToSquareZeroEquivLift_symm_apply_apply_coe`, `MvPolynomial.restrictScalars_restrictSupportIdeal`, `restrictScalars_inj`, `restrictScalars_sup`, `KaehlerDifferential.submodule_span_range_eq_ideal`, `restrictScalars_injective`, `Ideal.restrictScalars_mul`, `Algebra.Extension.Hom.subToKer_apply_coe`, `traceDual_eq_span_map_traceDual_of_linearDisjoint`, `Ideal.smul_restrictScalars`, `Algebra.Extension.H1Cotangent.map_apply_coe`, `restrictScalars_mem`, `restrictScalars.isScalarTower`, `toAddSubmonoid_restrictScalars`, `restrictScalars_iSup`, `Subalgebra.restrictScalars_toSubmodule`, `restrictScalars_iInf`, `restrictScalars_eq_top_iff`, `KaehlerDifferential.range_kerCotangentToTensor`, `restrictScalarsEmbedding_apply`, `restrictScalars_localized'`, `Polynomial.ker_modByMonicHom`, `restrictScalars_sInf`, `Algebra.idealMap_apply_coe`, `le_traceDual_iff_map_le_one`, `KaehlerDifferential.kerTotal_map'`, `Ideal.map_includeLeft_eq`, `restrictScalars_pow`, `Algebra.Generators.H1Cotangent.equiv_apply`, `Quotient.restrictScalarsEquiv_mk`, `LinearMap.range_restrictScalars`, `restrictScalars_self`, `restrictScalars_inf`, `restrictScalars_localized'_smul`, `span_coe_eq_restrictScalars`, `restrictScalarsEquiv_apply`, `span_smul_of_span_eq_top`, `restrictScalars_map`, `restrictScalars_span`
`restrictScalarsEmbedding` 📖	CompOp	1 math math: `restrictScalarsEmbedding_apply`
`restrictScalarsEquiv` 📖	CompOp	2 math math: `restrictScalarsEquiv_symm_apply`, `restrictScalarsEquiv_apply`
`restrictScalarsLatticeHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_restrictScalars` 📖	mathematical	—	`SetLike.coe` `Submodule` `setLike` `restrictScalars`	—	—
`restrictScalarsEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelEmbedding.instFunLike` `restrictScalarsEmbedding` `restrictScalars`	—	—
`restrictScalarsEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `SetLike.instMembership` `setLike` `restrictScalars` `addCommMonoid` `restrictScalars.origModule` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `restrictScalarsEquiv`	—	`RingHomInvPair.ids`
`restrictScalarsEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `SetLike.instMembership` `setLike` `restrictScalars` `addCommMonoid` `module` `restrictScalars.origModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `restrictScalarsEquiv`	—	`RingHomInvPair.ids`
`restrictScalars_bot` 📖	mathematical	—	`restrictScalars` `Bot.bot` `Submodule` `instBot`	—	—
`restrictScalars_eq_bot_iff` 📖	mathematical	—	`restrictScalars` `Bot.bot` `Submodule` `instBot`	—	—
`restrictScalars_eq_top_iff` 📖	mathematical	—	`restrictScalars` `Top.top` `Submodule` `instTop`	—	—
`restrictScalars_iInf` 📖	mathematical	—	`restrictScalars` `iInf` `Submodule` `instInfSet`	—	`ext`
`restrictScalars_iSup` 📖	mathematical	—	`restrictScalars` `iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice`	—	`map_iSup` `FrameHomClass.tosSupHomClass` `CompleteLatticeHomClass.toFrameHomClass` `CompleteLatticeHom.instCompleteLatticeHomClass`
`restrictScalars_inf` 📖	mathematical	—	`restrictScalars` `Submodule` `instMin`	—	`ext`
`restrictScalars_inj` 📖	mathematical	—	`restrictScalars`	—	`restrictScalars_injective`
`restrictScalars_injective` 📖	mathematical	—	`Submodule` `restrictScalars`	—	`ext` `Set.ext_iff` `SetLike.ext'_iff`
`restrictScalars_le` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `restrictScalars`	—	—
`restrictScalars_lt` 📖	mathematical	—	`Submodule` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `restrictScalars`	—	—
`restrictScalars_mem` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `setLike` `restrictScalars`	—	—
`restrictScalars_mono` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`restrictScalars`	—	`restrictScalars_monotone`
`restrictScalars_monotone` 📖	mathematical	—	`Monotone` `Submodule` `PartialOrder.toPreorder` `instPartialOrder` `restrictScalars`	—	`OrderEmbedding.monotone`
`restrictScalars_sInf` 📖	mathematical	—	`restrictScalars` `InfSet.sInf` `Submodule` `instInfSet` `Set.image`	—	`ext`
`restrictScalars_sSup` 📖	mathematical	—	`restrictScalars` `SupSet.sSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Set.image`	—	`toAddSubmonoid_sSup` `Set.image_congr`
`restrictScalars_self` 📖	mathematical	—	`restrictScalars` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`SetLike.coe_injective` `IsScalarTower.left`
`restrictScalars_sup` 📖	mathematical	—	`restrictScalars` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice`	—	`restrictScalars.congr_simp` `sSup_insert` `sSup_singleton` `Set.image_insert_eq` `Set.image_singleton` `restrictScalars_sSup`
`restrictScalars_top` 📖	mathematical	—	`restrictScalars` `Top.top` `Submodule` `instTop`	—	—
`toAddSubmonoid_restrictScalars` 📖	mathematical	—	`toAddSubmonoid` `restrictScalars`	—	—
`toIntSubmodule_toAddSubgroup` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `AddSubgroup` `AddCommGroup.toAddGroup` `Submodule` `Int.instSemiring` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `instPartialOrder` `instFunLikeOrderIso` `AddSubgroup.toIntSubmodule` `toAddSubgroup` `restrictScalars` `Ring.toSemiring` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddCommGroup.intIsScalarTower`	—	—

Submodule.restrictScalars

Definitions

Name	Category	Theorems
`origModule` 📖	CompOp	5 math math: `Submodule.span_range_inclusion_restrictScalars_eq_top`, `Submodule.span_range_inclusion_eq_top`, `Submodule.restrictScalarsEquiv_symm_apply`, `isScalarTower`, `Submodule.restrictScalarsEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.restrictScalars` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule.addCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `origModule` `Submodule.smul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `DistribMulAction.toMulAction`	—	`IsScalarTower.left` `smul_assoc`

---

← Back to Index