Theorem algebraMap_strictMono

Modification history

2026-04-01 19:38
Mathlib/Algebra/Order/Algebra.lean
chore(Algebra/Order): generalise ordered algebra lemmas (#37040) …
Modified algebraMap_strictMonoView on Github →
2025-12-18 16:09
Mathlib/Algebra/Order/Algebra.lean
chore(Algebra/Order): deduplicate material on ordered algebras (#32937)
Modified algebraMap_strictMonoView on Github →
2025-10-27 16:35
Mathlib/Algebra/Order/Module/Algebra.lean
feat(gcongr): support `@[gcongr]` for `Monotone` and friends (#28339) …
Modified algebraMap_strictMonoView on Github →
2024-01-24 02:51
Mathlib/Algebra/Order/Module/Algebra.lean
feat: `n • v` and `v` are on the same ray (#9104) …
Added algebraMap_strictMonoView on Github →