Extension

📁 Source: Mathlib/RingTheory/Valuation/Extension.lean

Statistics

Metric	Count
Definitions `HasExtension`, `instAlgebraInteger`, `instAlgebra_valuationSubring`	3
Theorems `algebraMap_injective`, `algebraMap_mem_maximalIdeal_iff`, `algebraMap_mem_valuationSubring`, `algebraMap_residue_eq_residue_algebraMap`, `coe_algebraMap_valuationSubring_eq`, `id`, `instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap`, `instIsLocalHomValuationInteger`, `instIsScalarTowerInteger`, `instIsScalarTower_valuationSubring`, `instIsScalarTower_valuationSubring'`, `instIsTorsionFreeInteger`, `instLiesOverSubtypeMemValuationSubringValuationSubringMaximalIdeal`, `maximalIdeal_comap_algebraMap_eq_maximalIdeal`, `mk_smul_mk`, `ofComapInteger`, `val_algebraMap`, `val_isEquiv_comap`, `val_map_eq_iff`, `val_map_eq_one_iff`, `val_map_le_iff`, `val_map_le_one_iff`, `val_map_lt_iff`, `val_map_lt_one_iff`, `val_smul`	25
Total	28

Valuation

Definitions

Name	Category	Theorems
`HasExtension` 📖	CompData	2 math math: `HasExtension.ofComapInteger`, `HasExtension.id`

Valuation.HasExtension

Definitions

Name	Category	Theorems
`instAlgebraInteger` 📖	CompOp	7 math math: `val_algebraMap`, `instIsLocalHomValuationInteger`, `instIsTorsionFreeInteger`, `mk_smul_mk`, `algebraMap_injective`, `instIsScalarTowerInteger`, `val_smul`
`instAlgebra_valuationSubring` 📖	CompOp	7 math math: `instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap`, `maximalIdeal_comap_algebraMap_eq_maximalIdeal`, `instIsScalarTower_valuationSubring'`, `coe_algebraMap_valuationSubring_eq`, `instLiesOverSubtypeMemValuationSubringValuationSubringMaximalIdeal`, `algebraMap_residue_eq_residue_algebraMap`, `algebraMap_mem_maximalIdeal_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_injective` 📖	mathematical	—	`Subring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `Subring.instSubringClass` `Ring.toSemiring` `Subring.toRing` `RingHom.instFunLike` `algebraMap` `instAlgebraInteger`	—	`FaithfulSMul.algebraMap_injective` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `Subring.instIsDomainSubtypeMem` `instIsDomain` `Subring.instNontrivialSubtypeMem` `instIsTorsionFreeInteger` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`algebraMap_mem_maximalIdeal_iff` 📖	mathematical	—	`ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Ideal` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `ValuationSubring.instSubringClass` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsLocalRing.maximalIdeal` `ValuationSubring.isLocalRing` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `instAlgebra_valuationSubring`	—	`SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `ValuationSubring.isLocalRing` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap`
`algebraMap_mem_valuationSubring` 📖	mathematical	—	`ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap`	—	`Valuation.mem_valuationSubring_iff` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `val_map_le_iff`
`algebraMap_residue_eq_residue_algebraMap` 📖	mathematical	—	`DFunLike.coe` `RingHom` `IsLocalRing.ResidueField` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `ValuationSubring.instCommRingSubtypeMem` `ValuationSubring.isLocalRing` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `IsLocalRing.ResidueField.instAlgebra` `instAlgebra_valuationSubring` `instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap` `CommRing.toCommSemiring` `IsLocalRing.residue` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `ValuationSubring.instSubringClass`	—	`ValuationSubring.isLocalRing` `instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap`
`coe_algebraMap_valuationSubring_eq` 📖	mathematical	—	`ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `ValuationSubring.instSubringClass` `RingHom.instFunLike` `algebraMap` `instAlgebra_valuationSubring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass`
`id` 📖	mathematical	—	`Valuation.HasExtension` `CommRing.toRing` `Algebra.id` `CommRing.toCommSemiring`	—	`Valuation.comap_id`
`instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap` 📖	mathematical	—	`IsLocalHom` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `ValuationSubring.instSubringClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike` `algebraMap` `instAlgebra_valuationSubring`	—	`instIsLocalHomValuationInteger` `instIsLocalHomOfMonoidWithZeroHomClassOfNontrivial` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`instIsLocalHomValuationInteger` 📖	mathematical	—	`IsLocalHom` `Subring` `Ring.toNonAssocRing` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Subring.instSubringClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike` `algebraMap` `instAlgebraInteger`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Valuation.Integers.isUnit_of_one` `Valuation.integer.integers` `isUnit_map_iff` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsUnit.map` `val_map_eq_one_iff` `Valuation.Integers.one_of_isUnit`
`instIsScalarTowerInteger` 📖	mathematical	—	`IsScalarTower` `Subring` `Ring.toNonAssocRing` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `Algebra.toSMul` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Subring.instSubringClass` `Ring.toSemiring` `Subring.toRing` `instAlgebraInteger` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Subsemiring.instModuleSubtypeMem` `Semiring.toModule` `Algebra.ofSubring`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Algebra.smul_def` `mul_assoc`
`instIsScalarTower_valuationSubring` 📖	mathematical	—	`IsScalarTower` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Algebra.toSMul` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `ValuationSubring.instSubringClass` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ValuationSubring.instAlgebraSubtypeMem` `Algebra.ofSubsemiring`	—	—
`instIsScalarTower_valuationSubring'` 📖	mathematical	—	`IsScalarTower` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Algebra.toSMul` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `ValuationSubring.instSubringClass` `CommSemiring.toSemiring` `instAlgebra_valuationSubring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ValuationSubring.instAlgebraSubtypeMem` `Algebra.ofSubsemiring`	—	`instIsScalarTowerInteger`
`instIsTorsionFreeInteger` 📖	mathematical	—	`Module.IsTorsionFree` `Subring` `Ring.toNonAssocRing` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Subring.instSubringClass` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Subring.toRing` `Algebra.toModule` `Ring.toSemiring` `instAlgebraInteger`	—	`Module.IsTorsionFree.of_smul_eq_zero` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Subring.instNontrivialSubtypeMem` `IsDomain.toNontrivial` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `val_map_le_one_iff` `Algebra.smul_def` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass` `IsDomain.toIsCancelMulZero`
`instLiesOverSubtypeMemValuationSubringValuationSubringMaximalIdeal` 📖	mathematical	—	`Ideal.LiesOver` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `ValuationSubring.instSubringClass` `CommSemiring.toSemiring` `instAlgebra_valuationSubring` `IsLocalRing.maximalIdeal` `ValuationSubring.isLocalRing`	—	`SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `ValuationSubring.isLocalRing` `RingHom.instRingHomClass` `maximalIdeal_comap_algebraMap_eq_maximalIdeal`
`maximalIdeal_comap_algebraMap_eq_maximalIdeal` 📖	mathematical	—	`Ideal.comap` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `ValuationSubring.instSubringClass` `RingHom.instFunLike` `algebraMap` `instAlgebra_valuationSubring` `RingHom.instRingHomClass` `IsLocalRing.maximalIdeal` `ValuationSubring.isLocalRing`	—	`Ideal.ext` `SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `RingHom.instRingHomClass` `ValuationSubring.isLocalRing` `Ideal.mem_comap` `algebraMap_mem_maximalIdeal_iff`
`mk_smul_mk` 📖	mathematical	`Subring` `Ring.toNonAssocRing` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer`	`Subring` `Ring.toNonAssocRing` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `Algebra.toSMul` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Subring.instSubringClass` `Ring.toSemiring` `Subring.toRing` `instAlgebraInteger` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `SubsemiringClass.toSubmonoidClass` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation` `Valuation.instFunLike` `MulOne.toOne` `MulOneClass.toMulOne` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero` `val_map_le_one_iff` `Algebra.smul_def`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass`
`ofComapInteger` 📖	mathematical	`Subring.comap` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `Ring.toNonAssocRing` `algebraMap` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `Valuation.integer` `DivisionRing.toRing` `Field.toDivisionRing`	`Valuation.HasExtension` `Field.toCommRing` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	`Valuation.isEquiv_iff_val_le_one`
`val_algebraMap` 📖	mathematical	—	`Subring` `Ring.toNonAssocRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `DFunLike.coe` `RingHom` `CommRing.toRing` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Subring.instSubringClass` `Ring.toSemiring` `Subring.toRing` `RingHom.instFunLike` `algebraMap` `instAlgebraInteger`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass`
`val_isEquiv_comap` 📖	mathematical	—	`Valuation.IsEquiv` `CommRing.toRing` `Valuation.comap` `algebraMap` `CommRing.toCommSemiring` `Ring.toSemiring`	—	—
`val_map_eq_iff` 📖	mathematical	—	`DFunLike.coe` `Valuation` `Valuation.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `CommRing.toRing`	—	`Valuation.IsEquiv.eq_iff` `val_isEquiv_comap`
`val_map_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `Valuation` `Valuation.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero` `CommRing.toRing`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `val_map_le_iff`
`val_map_le_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `DFunLike.coe` `Valuation` `Valuation.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `CommRing.toRing`	—	`Valuation.IsEquiv.symm` `val_isEquiv_comap`
`val_map_le_one_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `DFunLike.coe` `Valuation` `Valuation.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero` `CommRing.toRing`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `val_map_le_iff`
`val_map_lt_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `DFunLike.coe` `Valuation` `Valuation.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `CommRing.toRing`	—	`Iff.not` `val_map_le_iff`
`val_map_lt_one_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `DFunLike.coe` `Valuation` `Valuation.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero` `CommRing.toRing`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Iff.not` `val_map_le_iff`
`val_smul` 📖	mathematical	—	`Subring` `Ring.toNonAssocRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `CommRing.toRing` `Algebra.toSMul` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Subring.instSubringClass` `Ring.toSemiring` `Subring.toRing` `instAlgebraInteger`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass`

---

← Back to Index