Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_monoid_algebra.op_ring_equiv_symm_single

Modification history

2021-11-19 12:03
src/algebra/monoid_algebra/basic.lean
refactor(algebra/opposites): use mul_opposite for multiplicative opposite (#10302) …
Modified add_monoid_algebra.op_ring_equiv_symm_singleView on Github →
2021-08-18 18:52
src/algebra/monoid_algebra.lean
feat(algebra/monoid_algebra): add_monoid_algebra.op_{add,ring}_equiv (#8536) …
Added add_monoid_algebra.op_ring_equiv_symm_singleView on Github →