Theorem Algebra.lmul_isUnit_iff

Modification history

2024-01-10 09:09
Mathlib/Algebra/Algebra/Bilinear.lean
feat: Add Basis.of_isLocalizedModule (#9210) …
Added Algebra.lmul_isUnit_iffView on Github →