Theorem AlgEquiv.toRingEquiv_toOpposite

Modification history

2026-02-17 23:08
Mathlib/Algebra/Algebra/Opposite.lean
chore: bump toolchain to v4.29.0-rc1 (#35459)
Modified AlgEquiv.toRingEquiv_toOppositeView on Github →
2023-08-11 11:56
Mathlib/Algebra/Algebra/Opposite.lean
feat(Algebra/Algebra/Opposite): tools for working with opposite algebras (#6364) …
Added AlgEquiv.toRingEquiv_toOppositeView on Github →