Def add_monoid_algebra.to_multiplicative_alg_equiv

Modification history

2021-04-30 10:14
src/algebra/monoid_algebra.lean
feat(ring_theory/finiteness): add add_monoid_algebra.ft_of_fg (#7265) …
Added add_monoid_algebra.to_multiplicative_alg_equivView on Github →