Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-20 10:39
7c8c9643
View on Github →
feat: port LinearAlgebra.AdicCompletion (
#4133
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/LinearAlgebra/AdicCompletion.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
IsAdicComplete.le_jacobson_bot
added
theorem
IsHausdorff.haus
added
theorem
IsHausdorff.iInf_pow_smul
added
theorem
IsPrecomplete.prec
added
theorem
adicCompletion.coe_eval
added
def
adicCompletion.eval
added
theorem
adicCompletion.eval_apply
added
theorem
adicCompletion.eval_comp_of
added
theorem
adicCompletion.eval_of
added
theorem
adicCompletion.ext
added
def
adicCompletion.of
added
theorem
adicCompletion.of_apply
added
theorem
adicCompletion.range_eval
added
def
adicCompletion
added
theorem
isHausdorff_iff
added
theorem
isPrecomplete_iff