Theorem WithBot.unbot_inj

Modification history

2026-03-25 15:49
Mathlib/Order/WithBot.lean
feat(RingTheory/Length): length of a module along a quotient map (#37126) …
Added WithBot.unbot_injView on Github →