Theorem Unitization.toProd_inj_iff

Modification history

2026-03-25 16:54
Mathlib/Algebra/Algebra/Unitization.lean
refactor: make `Unitization` into a one-field structure (#37014) …
Added Unitization.toProd_inj_iffView on Github →