Def AlgEquivClass.toAlgEquiv

Modification history

2026-09-09 08:54
Mathlib/Algebra/Algebra/Equiv.lean
chore: rename Alg{Hom,Equiv}Class.toAlg{Hom,Equiv} to Alg{Hom,Equiv}.ofClass (#43557) …
Deleted AlgEquivClass.toAlgEquivView on Github →
2023-08-19 12:28
Mathlib/Algebra/Algebra/Equiv.lean
chore: make sure that some coercions have an attached definition (#6667)
Added AlgEquivClass.toAlgEquivView on Github →