Theorem AlgEquiv.apply_ofClass_symm_apply

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) …

Added AlgEquiv.apply_ofClass_symm_apply View on Github →