Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.mem_to_add_submonoid

Modification history

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