Mathlib Changelog
Changelog
About
Github
Commit
2020-07-28 02:35
005201a2
View on Github →
feat(linear_algebra/adic_completion): basic definitions about completions of modules (
#3452
)
Estimated changes
Created
src/linear_algebra/adic_completion.lean
added
theorem
Hausdorffification.induction_on
added
def
Hausdorffification.lift
added
theorem
Hausdorffification.lift_comp_of
added
theorem
Hausdorffification.lift_eq
added
theorem
Hausdorffification.lift_of
added
def
Hausdorffification.of
added
def
Hausdorffification
added
theorem
adic_completion.coe_eval
added
def
adic_completion.eval
added
theorem
adic_completion.eval_apply
added
theorem
adic_completion.eval_comp_of
added
theorem
adic_completion.eval_of
added
theorem
adic_completion.ext
added
def
adic_completion.of
added
theorem
adic_completion.of_apply
added
theorem
adic_completion.range_eval
added
def
adic_completion
added
theorem
is_Hausdorff.infi_pow_smul
added
def
is_Hausdorff
added
def
is_adic_complete
added
def
is_precomplete
Created
src/linear_algebra/smodeq.lean
added
theorem
smodeq.add
added
theorem
smodeq.bot
added
theorem
smodeq.comap
added
theorem
smodeq.map
added
theorem
smodeq.mono
added
theorem
smodeq.refl
added
theorem
smodeq.smul
added
theorem
smodeq.symm
added
theorem
smodeq.top
added
theorem
smodeq.trans
added
theorem
smodeq.zero
added
def
smodeq
Modified
src/ring_theory/ideal_operations.lean
added
theorem
ideal.top_pow
added
theorem
submodule.map_smul''