Theorem RingEquiv.toIntAlgEquiv_injective

Modification history

2026-07-27 15:11
Mathlib/Algebra/Algebra/Equiv.lean
feat(Algebra/Algebra): reinterpret a RingEquiv as a ℕ/ℤ/ℚ-algebra isomorphism (#40298) …
Added RingEquiv.toIntAlgEquiv_injectiveView on Github →