Commit 2025-11-18 22:57 48d1fe28
View on Github →refactor: make ⇑e⁻¹ = ⇑e.symm simp (#27433)
The motivation here is that the spelling ⇑e⁻¹ is only available when e is an automorphism, while the ⇑e.symm one is available for all isomorphisms. However we do not want to simplify e⁻¹ = e.symm (without the coercions to function) since e⁻¹ is an algebraic expression and e.symm is not. We consider that applying the coercion to functions gets us out of algebra land, and therefore it is okay to "dealgebraise" the expression further.
From BrauerGroup and ClassFieldTheory