Structures · Algebra
IsPrecomplete
A module M is precomplete with respect to an ideal I if every Cauchy sequence converges.
- Defined in
- Mathlib.RingTheory.AdicCompletion.Basic
- Shape
- 2 explicit arguments · adds prec'
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 by24
- PowerSeries.IsWeierstrassDivisorAt.div
- PowerSeries.IsWeierstrassDivisorAt.mod
- PowerSeries.weierstrassMod
- PowerSeries.weierstrassDiv
- Perfection.teichmullerFun
- PowerSeries.IsWeierstrassDivisorAt.divCoeff
- Perfection.teichmullerFun_sModEq
- IsPrecomplete.prec'
- surjective_of_mkQ_comp_surjective
- AdicCompletion.of_surjective
- PowerSeries.IsWeierstrassDivisorAt.mod.congr_simp
- Perfection.exists_teichmullerFun
- PowerSeries.weierstrassDiv_zero_right
- surjective_of_mk_map_comp_surjective
- PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem
- PowerSeries.weierstrassMod_zero_right
- PowerSeries.IsWeierstrassDivisorAt.coeff_div
- PowerSeries.weierstrassDiv_zero
- PowerSeries.weierstrassMod_zero
- PowerSeries.weierstrassDiv.congr_simp
- PowerSeries.IsWeierstrassDivisorAt.divCoeff.congr_simp
- PowerSeries.degree_weierstrassMod_lt
- PowerSeries.IsWeierstrassDivisorAt.div.congr_simp
- PowerSeries.weierstrassMod.congr_simp
Ancestors0
No ancestors.