Documentation Verification Report

Algebra

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

Statistics

Metric	Count
Definitions `evalAlgebraMap`	1
Theorems `algebraMap_le_algebraMap`, `algebraMap_lt_algebraMap`, `algebraMap_mono`, `algebraMap_nonneg`, `algebraMap_pos`, `algebraMap_strictMono`	6
Total	7

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalAlgebraMap` 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_le_algebraMap` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`Algebra.algebraMap_eq_smul_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`algebraMap_lt_algebraMap` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`Algebra.algebraMap_eq_smul_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`algebraMap_mono` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`Algebra.algebraMap_eq_smul_one` `smul_le_smul_of_nonneg_right` `zero_le_one` `IsOrderedRing.toZeroLEOneClass`
`algebraMap_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap_mono`
`algebraMap_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap_strictMono`
`algebraMap_strictMono` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`Algebra.algebraMap_eq_smul_one` `smul_lt_smul_of_pos_right` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`

---

← Back to Index