Mathlib v3 is deprecated. Go to Mathlib v4

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''