Commit 2024-11-03 08:14 43eb2160

View on Github →

chore(Algebra/Module/Submodule): split Submodule/Basic.lean (#18489) This PR splits off the definition of Submodule into a new file Submodule/Defs.lean, with the goal of reducing the theory needed to define submodules (and eventually, to define the ideal quotient).

  • master: 0.896884 per-decl; 0.605522 per-module
  • split-Submodule.Basic: 0.896884 per-decl; 0.605552 per-module

Estimated changes

deleted theorem Submodule.carrier_inj
deleted theorem Submodule.coe_add
deleted theorem Submodule.coe_copy
deleted theorem Submodule.coe_eq_zero
deleted theorem Submodule.coe_mem
deleted theorem Submodule.coe_mk
deleted theorem Submodule.coe_set_mk
deleted theorem Submodule.coe_smul
deleted theorem Submodule.coe_zero
deleted theorem Submodule.copy_eq
deleted theorem Submodule.eta
deleted theorem Submodule.ext
deleted theorem Submodule.mem_carrier
deleted theorem Submodule.mem_mk
deleted theorem Submodule.mk_eq_zero
deleted theorem Submodule.mk_le_mk
deleted theorem Submodule.smul_mem
deleted theorem Submodule.smul_mem_iff'
deleted structure Submodule
added theorem Submodule.carrier_inj
added theorem Submodule.coe_add
added theorem Submodule.coe_copy
added theorem Submodule.coe_eq_zero
added theorem Submodule.coe_mem
added theorem Submodule.coe_mk
added theorem Submodule.coe_set_mk
added theorem Submodule.coe_smul
added theorem Submodule.coe_zero
added theorem Submodule.copy_eq
added theorem Submodule.eta
added theorem Submodule.ext
added theorem Submodule.mem_carrier
added theorem Submodule.mem_mk
added theorem Submodule.mk_eq_zero
added theorem Submodule.mk_le_mk
added theorem Submodule.smul_mem
added structure Submodule
added theorem Ideal.sum_mem
deleted theorem Ideal.sum_mem