Theorem AlgHom.toRingHom_fromOpposite

Modification history

2023-08-11 11:56
Mathlib/Algebra/Algebra/Opposite.lean
feat(Algebra/Algebra/Opposite): tools for working with opposite algebras (#6364) …
Added AlgHom.toRingHom_fromOppositeView on Github →