Mathlib v3 is deprecated. Go to Mathlib v4

Theorem monoid_algebra.op_ring_equiv_single

Modification history

2021-08-18 18:52
src/algebra/monoid_algebra.lean
feat(algebra/monoid_algebra): add_monoid_algebra.op_{add,ring}_equiv (#8536) …
Added monoid_algebra.op_ring_equiv_singleView on Github →