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