Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-28 21:23 ccd37746

View on Github →

chore(ring_theory/*): dot notation for submodule.fg and subalgebra.fg (#13737)

Estimated changes

added theorem subalgebra.fg.map
added theorem subalgebra.fg.prod
deleted theorem subalgebra.fg_map
deleted theorem subalgebra.fg_prod
added theorem submodule.fg.mul
added theorem submodule.fg.pow
added theorem submodule.fg.prod
added theorem submodule.fg.sup
deleted theorem submodule.fg_mul
deleted theorem submodule.fg_pow
deleted theorem submodule.fg_prod
deleted theorem submodule.fg_sup