Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-10 21:33 5cdebb75

View on Github →

feat(*): Miscellaneous lemmas in algebra (#1188)

Trying things out
feat(ring_theory/*): Misc little lemmas
More little lemmas

Estimated changes

Modified src/group_theory/subgroup.lean

deleted theorem add_group.closure_mono

deleted theorem add_group.mclosure_inv_subset

deleted theorem add_group.mclosure_subset

added theorem group.closure_subgroup

Modified src/ring_theory/algebra.lean

added theorem span_int_eq

added theorem span_int_eq_add_group_closure

Modified src/ring_theory/algebra_operations.lean

added theorem submodule.mul_subset_mul

added theorem submodule.pow_subset_pow

added theorem submodule.smul_def

added theorem submodule.smul_le_smul

added theorem submodule.smul_singleton

Modified src/ring_theory/ideal_operations.lean

added theorem ideal.map_quotient_self

added theorem ideal.pow_le_pow

Modified src/ring_theory/ideals.lean

added theorem ideal.eq_bot_of_prime

added theorem ideal.eq_bot_or_top

Modified src/ring_theory/noetherian.lean

added theorem submodule.fg_pow