Structures · Algebra
IsHausdorff
A module M is Hausdorff with respect to an ideal I if ⋂ I^n M = 0.
- Defined in
- Mathlib.RingTheory.AdicCompletion.Basic
- Shape
- 2 explicit arguments · adds haus'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by21
- PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add
- IsHausdorff.eq_iff_smodEq
- PowerSeries.IsWeierstrassFactorization.elim
- IsHausdorff.haus'
- PowerSeries.IsWeierstrassDivision.elim
- Hausdorffification.lift
- surjective_of_mkQ_comp_surjective
- AdicCompletion.of_injective
- surjective_of_mk_map_comp_surjective
- AdicCompletion.of_inj
- PowerSeries.IsWeierstrassDivisorAt.eq_zero_of_mul_eq
- IsHausdorff.funext
- Hausdorffification.lift_of
- IsHausdorff.funext'
- IsHausdorff.StrictMono.funext'
- IsHausdorff.StrictMono.funext
- Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt'
- PowerSeries.IsWeierstrassDivision.eq_zero
- Hausdorffification.lift_eq
- IsHausdorff.of_map
- Hausdorffification.lift_comp_of
Ancestors0
No ancestors.