Def AlgEquiv.uniqueProd

Modification history

2025-05-06 11:37
Mathlib/Algebra/Algebra/Prod.lean
feat: add {Alg,Linear}Equiv.{prodUnique,uniqueProd} (#24168) …
Added AlgEquiv.uniqueProdView on Github →