Documentation Verification Report

Tower

📁 Source: Mathlib/Algebra/Algebra/Tower.lean

Statistics

Metric	Count
Definitions `extendScalarsOfSurjective`, `restrictScalars`, `extendScalarsOfSurjective`, `restrictScalars`, `lsmul`, `toAlgHom`	6
Theorems `coe_restrictScalars`, `coe_restrictScalars'`, `coe_restrictScalars_symm`, `coe_restrictScalars_symm'`, `extendScalarsOfSurjective_apply`, `extendScalarsOfSurjective_symm`, `restrictScalars_apply`, `restrictScalars_extendScalarsOfSurjective`, `restrictScalars_injective`, `restrictScalars_symm_apply`, `coe_restrictScalars`, `coe_restrictScalars'`, `comp_algebraMap_of_tower`, `extendScalarsOfSurjective_apply`, `map_algebraMap`, `restrictScalars_apply`, `restrictScalars_extendScalarsOfSurjective`, `restrictScalars_injective`, `algebraMapSubmonoid_map_map`, `lsmul_coe`, `lsmul_injective`, `ext`, `ext_iff`, `algebraMap_apply`, `algebraMap_eq`, `algebraMap_smul`, `coe_toAlgHom`, `coe_toAlgHom'`, `of_algHom`, `of_algebraMap_eq`, `of_algebraMap_eq'`, `of_algebraMap_smul`, `of_compHom`, `subsemiring`, `toAlgHom_apply`, `coe_span_eq_span_of_surjective`, `map_mem_span_algebraMap_image`, `restrictScalars_span`, `smul_mem_span_smul`, `smul_mem_span_smul'`, `smul_mem_span_smul_of_mem`, `span_algebraMap_image`, `span_algebraMap_image_of_tower`, `span_smul_of_span_eq_top`	44
Total	50

AlgEquiv

Definitions

Name	Category	Theorems
`extendScalarsOfSurjective` 📖	CompOp	3 math math: `extendScalarsOfSurjective_symm`, `restrictScalars_extendScalarsOfSurjective`, `extendScalarsOfSurjective_apply`
`restrictScalars` 📖	CompOp	11 math math: `coe_restrictScalars_symm`, `MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval`, `restrictScalars_symm_apply`, `coe_restrictScalars'`, `coe_restrictScalars`, `restrictScalars_apply`, `IsFractionRing.restrictScalars_fieldEquivOfAlgEquiv`, `Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv`, `restrictScalars_injective`, `coe_restrictScalars_symm'`, `restrictScalars_extendScalarsOfSurjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_restrictScalars` 📖	mathematical	—	`RingEquivClass.toRingEquiv` `AlgEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `instEquivLike` `AlgEquivClass.toRingEquivClass` `instAlgEquivClass` `restrictScalars`	—	`AlgEquivClass.toRingEquivClass` `instAlgEquivClass`
`coe_restrictScalars'` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `instFunLike` `restrictScalars`	—	—
`coe_restrictScalars_symm` 📖	mathematical	—	`RingEquivClass.toRingEquiv` `AlgEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `instEquivLike` `AlgEquivClass.toRingEquivClass` `instAlgEquivClass` `symm` `restrictScalars`	—	`AlgEquivClass.toRingEquivClass` `instAlgEquivClass`
`coe_restrictScalars_symm'` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `instFunLike` `symm` `restrictScalars`	—	—
`extendScalarsOfSurjective_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`DFunLike.coe` `AlgEquiv` `instFunLike` `extendScalarsOfSurjective` `EquivLike.toFunLike` `instEquivLike`	—	—
`extendScalarsOfSurjective_symm` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`symm` `extendScalarsOfSurjective`	—	—
`restrictScalars_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `instFunLike` `restrictScalars`	—	—
`restrictScalars_extendScalarsOfSurjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`restrictScalars` `extendScalarsOfSurjective`	—	—
`restrictScalars_injective` 📖	mathematical	—	`AlgEquiv` `restrictScalars`	—	`ext` `congr_fun`
`restrictScalars_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `instFunLike` `symm` `restrictScalars`	—	—

AlgHom

Definitions

Name	Category	Theorems
`extendScalarsOfSurjective` 📖	CompOp	2 math math: `extendScalarsOfSurjective_apply`, `restrictScalars_extendScalarsOfSurjective`
`restrictScalars` 📖	CompOp	16 math math: `MvPolynomial.universalFactorizationMap_comp_map`, `GradedAlgHom.restrictScalars_coe_algHom`, `Algebra.TensorProduct.ext_ring_iff`, `coe_restrictScalars`, `PowerSeries.substAlgHom_comp_substAlgHom`, `restrictScalars_injective`, `Algebra.TensorProduct.lift_comp_includeRight`, `restrictScalars_extendScalarsOfSurjective`, `ContinuousAlgHom.coe_restrictScalars`, `coe_restrictScalars'`, `Algebra.TensorProduct.ext_iff`, `restrictScalars_apply`, `Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq`, `Algebra.TensorProduct.map_restrictScalars_comp_includeRight`, `Algebra.TensorProduct.liftEquiv_symm_apply_coe`, `MvPowerSeries.substAlgHom_comp_substAlgHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_restrictScalars` 📖	mathematical	—	`RingHomClass.toRingHom` `AlgHom` `funLike` `Semiring.toNonAssocSemiring` `AlgHomClass.toRingHomClass` `algHomClass` `restrictScalars`	—	`AlgHomClass.toRingHomClass` `algHomClass`
`coe_restrictScalars'` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `funLike` `restrictScalars`	—	—
`comp_algebraMap_of_tower` 📖	mathematical	—	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHomClass.toRingHom` `AlgHom` `funLike` `AlgHomClass.toRingHomClass` `algHomClass` `algebraMap`	—	`RingHom.ext` `AlgHomClass.toRingHomClass` `algHomClass` `map_algebraMap`
`extendScalarsOfSurjective_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`DFunLike.coe` `AlgHom` `funLike` `extendScalarsOfSurjective`	—	—
`map_algebraMap` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `funLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsScalarTower.algebraMap_apply` `commutes`
`restrictScalars_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `funLike` `restrictScalars`	—	—
`restrictScalars_extendScalarsOfSurjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`restrictScalars` `extendScalarsOfSurjective`	—	—
`restrictScalars_injective` 📖	mathematical	—	`AlgHom` `restrictScalars`	—	`ext` `congr_fun`

Algebra

Definitions

Name	Category	Theorems
`lsmul` 📖	CompOp	8 math math: `lmul_algebraMap`, `lsmul_injective`, `Module.AEval.mem_mapSubmodule_symm_apply`, `toMatrix_lsmul`, `FormallyUnramified.comp_sec`, `TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor`, `Module.AEval.mem_mapSubmodule_apply`, `lsmul_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMapSubmonoid_map_map` 📖	mathematical	—	`algebraMapSubmonoid` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`algebraMapSubmonoid_map_eq`
`lsmul_coe` 📖	mathematical	—	`DFunLike.coe` `Module.End` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `AlgHom` `Module.End.instSemiring` `Module.End.instAlgebra` `IsScalarTower.to_smulCommClass'` `toSMul` `AlgHom.funLike` `lsmul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`IsScalarTower.to_smulCommClass'`
`lsmul_injective` 📖	mathematical	—	`DFunLike.coe` `Module.End` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `AlgHom` `Module.End.instSemiring` `Module.End.instAlgebra` `IsScalarTower.to_smulCommClass'` `toSMul` `AlgHom.funLike` `lsmul`	—	`smul_right_injective` `IsDomain.toIsCancelMulZero`

IsScalarTower

Definitions

Name	Category	Theorems
`toAlgHom` 📖	CompOp	56 math math: `MvPolynomial.algHom_ext'_iff`, `coe_toAlgHom'`, `IntermediateField.LinearDisjoint.map'`, `algebraicClosure.map_eq_of_algebraicClosure_eq_bot`, `adjoin_range_toAlgHom`, `IsLocalizedModule.map_linearMap_of_isLocalization`, `PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal`, `MvPolynomial.sumAlgEquiv_comp_rename_inr`, `MvPolynomial.aevalTower_toAlgHom`, `Subalgebra.range_isScalarTower_toAlgHom`, `Normal.algHomEquivAut_symm_apply`, `toAlgHom_comp_sectionOfRetractionKerToTensorAux`, `Ideal.Fiber.lift_residueField_surjective`, `IsDedekindDomain.range_sup_range_eq_top_of_isCoprime_differentIdeal`, `IntermediateField.linearDisjoint_iff`, `IntermediateField.map_fixingSubgroup`, `Polynomial.aevalTower_toAlgHom`, `normalClosure.restrictScalars_eq`, `KaehlerDifferential.End_equiv_aux`, `PrimeSpectrum.preimageEquivFiber_apply_asIdeal`, `Ideal.ResidueField.liftₐ_comp_toAlgHom`, `Algebra.lift_algHom_comp_left`, `IsLocalization.mk'_algebraMap_eq_mk'`, `isLocalizedModule_iff_isLocalization`, `coe_toAlgHom`, `Algebra.isPushout_iff`, `IntermediateField.linearDisjoint_comm'`, `Algebra.IsAlgebraic.instIsLocalizedModuleNonZeroDivisorsToLinearMapToAlgHom`, `IntermediateField.LinearDisjoint.map''`, `IntermediateField.LinearDisjoint.symm'`, `instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid`, `derivationToSquareZeroEquivLift_symm_apply_apply_coe`, `Algebra.IsPushout.out`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal`, `Ideal.ResidueField.algHom_ext_iff`, `IntermediateField.map_fixingSubgroup_index`, `Algebra.IsAlgebraic.isBaseChange_of_isFractionRing`, `IsLocalization.map_eq_toLinearMap_mapₐ`, `Algebra.lift_algHom_comp_right`, `toAlgHom_comp_sectionOfRetractionKerToTensor`, `PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal`, `Algebra.EssFiniteType.aux`, `Algebra.adjoin_restrictScalars`, `IsLocalization.mapExtendScalars_eq_toLinearMap_mapₐ`, `Module.Basis.localizationLocalization_span`, `MvPolynomial.aevalTower_comp_toAlgHom`, `derivationToSquareZeroEquivLift_apply_coe_apply`, `Algebra.IsPushout.cancelBaseChange_symm_comp_lTensor`, `Algebra.adjoin_algebraMap`, `IsLocalization.map_linearMap_eq_toLinearMap_mapₐ`, `separableClosure.map_eq_of_separableClosure_eq_bot`, `Polynomial.aevalTower_comp_toAlgHom`, `Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply`, `MvPolynomial.mapEquivMonic_symm_map_algebraMap`, `toAlgHom_apply`, `Algebra.Subalgebra.restrictScalars_adjoin`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`algebraMap_eq` `RingHom.comp_apply`
`algebraMap_eq` 📖	mathematical	—	`algebraMap` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`RingHom.ext` `Algebra.algebraMap_eq_smul_one` `smul_assoc` `one_smul`
`algebraMap_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`Algebra.algebraMap_eq_smul_one` `smul_assoc` `one_smul`
`coe_toAlgHom` 📖	mathematical	—	`RingHomClass.toRingHom` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike` `Semiring.toNonAssocSemiring` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `toAlgHom` `algebraMap`	—	`RingHom.ext` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`coe_toAlgHom'` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike` `toAlgHom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	—
`of_algHom` 📖	mathematical	—	`IsScalarTower` `Algebra.toSMul` `CommSemiring.toSemiring` `RingHom.toAlgebra` `AlgHom.toRingHom`	—	`of_algebraMap_eq` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.commutes`
`of_algebraMap_eq` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`IsScalarTower` `Algebra.toSMul` `CommSemiring.toSemiring`	—	`Algebra.smul_def` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_assoc`
`of_algebraMap_eq'` 📖	mathematical	`algebraMap` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`IsScalarTower` `Algebra.toSMul` `CommSemiring.toSemiring`	—	`of_algebraMap_eq` `RingHom.ext_iff`
`of_algebraMap_smul` 📖	mathematical	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`IsScalarTower` `Algebra.toSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`Algebra.smul_def` `SemigroupAction.mul_smul`
`of_compHom` 📖	mathematical	—	`IsScalarTower` `Algebra.toSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `CommSemiring.toSemiring` `MulAction.compHom` `MonoidHomClass.toMonoidHom` `RingHom` `Semiring.toNonAssocSemiring` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap`	—	`of_algebraMap_smul` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`subsemiring` 📖	mathematical	—	`IsScalarTower` `Subsemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Subsemiring.smul` `Algebra.toSMul` `Algebra.id`	—	`of_algebraMap_eq` `Subsemiring.instSubsemiringClass`
`toAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike` `toAlgHom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	—

IsScalarTower.Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Algebra.toSMul`	—	—	`Algebra.algebra_ext` `Algebra.smul_def` `mul_one`
`ext_iff` 📖	mathematical	—	`Algebra.toSMul`	—	`ext`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_span_eq_span_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`SetLike.coe` `Submodule` `setLike` `span` `CommSemiring.toSemiring`	—	`restrictScalars_span`
`map_mem_span_algebraMap_image` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `setLike` `span`	`Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `setLike` `span` `Set.image` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`RingHomSurjective.ids` `LinearMap.IsScalarTower.compatibleSMul'` `span_algebraMap_image_of_tower` `mem_map`
`restrictScalars_span` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`restrictScalars` `CommSemiring.toSemiring` `Algebra.toSMul` `span`	—	`LE.le.antisymm` `span_le_restrictScalars` `span_induction` `subset_span` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `addSubmonoidClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `algebraMap_smul` `smul_mem`
`smul_mem_span_smul` 📖	mathematical	`span` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Top.top` `Submodule` `instTop` `SetLike.instMembership` `setLike`	`Submodule` `SetLike.instMembership` `setLike` `span` `Set` `Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`span_smul_of_span_eq_top` `smul_mem` `span_le_restrictScalars`
`smul_mem_span_smul'` 📖	mathematical	`span` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Top.top` `Submodule` `instTop` `SetLike.instMembership` `setLike` `Set` `Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`Submodule` `SetLike.instMembership` `setLike` `span` `Set` `Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`span_smul_of_span_eq_top` `smul_mem`
`smul_mem_span_smul_of_mem` 📖	mathematical	`Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `setLike` `span` `Set` `Set.instMembership`	`Submodule` `SetLike.instMembership` `setLike` `span` `Set` `Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`span_induction` `subset_span` `Set.smul_mem_smul` `zero_smul` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `addSubmonoidClass` `add_smul` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `IsScalarTower.smul_assoc` `smul_mem`
`span_algebraMap_image` 📖	mathematical	—	`span` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Set.image` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `map` `Semiring.toModule` `RingHom.id` `RingHomSurjective.ids` `Algebra.linearMap`	—	`RingHomSurjective.ids` `span_image`
`span_algebraMap_image_of_tower` 📖	mathematical	—	`span` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Set.image` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `map` `RingHom.id` `RingHomSurjective.ids` `LinearMap.restrictScalars` `Semiring.toModule` `LinearMap.IsScalarTower.compatibleSMul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.linearMap`	—	`LinearMap.IsScalarTower.compatibleSMul'` `RingHomSurjective.ids` `span_image`
`span_smul_of_span_eq_top` 📖	mathematical	`span` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Top.top` `Submodule` `instTop`	`span` `Set` `Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `restrictScalars` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`le_antisymm` `span_le` `smul_mem` `subset_span` `closure_induction` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `addSubmonoidClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `span_induction` `zero_smul` `add_smul` `IsScalarTower.smul_assoc` `mem_top`

---

← Back to Index