Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_monoid_algebra.induction_on

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.induction_onView on Github →