Completion

📁 Source: Mathlib/Algebra/Order/CauSeq/Completion.lean

Statistics

Metric	Count
Definitions `commRing`, `divisionRing`, `instAddCauchy`, `instDivInvMonoid`, `instInhabitedCauchy`, `instIntCastCauchy`, `instInvCauchy`, `instMulCauchy`, `instNNRatCast`, `instNatCastCauchy`, `instNegCauchy`, `instOneCauchy`, `instPowCauchyNat`, `instRatCast`, `instReprCauchy`, `instSMulCauchyOfIsScalarTower`, `instSubCauchy`, `instZeroCauchy`, `mk`, `ofRat`, `ofRatRingHom`, `IsComplete`, `lim`	23
Theorems `instNonTrivial`, `cau_seq_zero_ne_one`, `inv_mk`, `inv_mul_cancel`, `inv_zero`, `mk_add`, `mk_eq`, `mk_eq_mk`, `mk_eq_zero`, `mk_mul`, `mk_neg`, `mk_pow`, `mk_smul`, `mk_sub`, `mul_inv_cancel`, `ofRatRingHom_apply`, `ofRat_add`, `ofRat_div`, `ofRat_injective`, `ofRat_intCast`, `ofRat_inv`, `ofRat_mul`, `ofRat_natCast`, `ofRat_neg`, `ofRat_nnratCast`, `ofRat_one`, `ofRat_ratCast`, `ofRat_sub`, `ofRat_zero`, `zero_ne_one`, `isComplete`, `complete`, `eq_lim_of_const_equiv`, `equiv_lim`, `le_lim`, `lim_add`, `lim_const`, `lim_eq_lim_of_equiv`, `lim_eq_of_equiv_const`, `lim_eq_zero_iff`, `lim_inv`, `lim_le`, `lim_lt`, `lim_mul`, `lim_mul_lim`, `lim_neg`, `lim_sub`, `lt_lim`	48
Total	71

CauSeq

Definitions

Name	Category	Theorems
`IsComplete` 📖	CompData	4 math math: `Complex.instIsComplete`, `Real.instIsCompleteAbs`, `PadicInt.complete`, `Padic.complete`
`lim` 📖	CompOp	25 math math: `Complex.lim_conj`, `le_lim`, `Complex.exp_def`, `lim_mul`, `lim_add`, `lt_lim`, `lim_const`, `equiv_lim`, `lim_eq_of_equiv_const`, `lim_eq_zero_iff`, `tendsto_limit`, `lim_sub`, `lim_lt`, `lim_le`, `Complex.lim_im`, `limit_zero_of_norm_tendsto_zero`, `lim_eq_lim_of_equiv`, `Complex.lim_norm`, `Padic.padicNormE_lim_le`, `lim_neg`, `lim_mul_lim`, `lim_inv`, `Complex.lim_re`, `eq_lim_of_const_equiv`, `Complex.lim_eq_lim_im_add_lim_re`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complete` 📖	mathematical	—	`CauSeq` `equiv` `const`	—	`IsComplete.isComplete`
`eq_lim_of_const_equiv` 📖	mathematical	`CauSeq` `equiv` `const`	`lim`	—	`const_equiv` `equiv_lim`
`equiv_lim` 📖	mathematical	—	`CauSeq` `equiv` `const` `lim`	—	`complete`
`le_lim` 📖	mathematical	`CauSeq` `DivisionRing.toRing` `Field.toDivisionRing` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instLEAbs` `const` `IsAbsoluteValue.abs_isAbsoluteValue`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `lim`	—	`IsAbsoluteValue.abs_isAbsoluteValue` `const_le` `le_of_le_of_eq` `equiv_lim`
`lim_add` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `lim` `CauSeq` `instAdd`	—	`eq_lim_of_const_equiv` `const_add` `add_sub_add_comm` `add_limZero` `equiv_lim`
`lim_const` 📖	mathematical	—	`lim` `const`	—	`lim_eq_of_equiv_const`
`lim_eq_lim_of_equiv` 📖	mathematical	`CauSeq` `equiv`	`lim`	—	`lim_eq_of_equiv_const` `equiv_lim`
`lim_eq_of_equiv_const` 📖	mathematical	`CauSeq` `equiv` `const`	`lim`	—	`eq_lim_of_const_equiv`
`lim_eq_zero_iff` 📖	mathematical	—	`lim` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `LimZero`	—	`equiv_lim` `limZero_congr` `const_limZero` `ext` `sub_zero` `lim_eq_of_equiv_const`
`lim_inv` 📖	mathematical	`LimZero` `DivisionRing.toRing` `Field.toDivisionRing`	`lim` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield`	—	`lim_eq_zero_iff` `lim_eq_of_equiv_const` `one_mul` `mul_assoc` `sub_mul` `mul_comm` `mul_limZero_right` `inv_mul_cancel` `sub_add` `sub_sub` `sub_add_eq_sub_sub` `sub_right_comm` `sub_limZero` `mul_right_comm` `const_inv` `limZero_congr` `mul_limZero_left` `equiv_lim`
`lim_le` 📖	mathematical	`CauSeq` `DivisionRing.toRing` `Field.toDivisionRing` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instLEAbs` `const` `IsAbsoluteValue.abs_isAbsoluteValue`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `lim`	—	`IsAbsoluteValue.abs_isAbsoluteValue` `const_le` `le_of_eq_of_le` `equiv_lim`
`lim_lt` 📖	mathematical	`CauSeq` `DivisionRing.toRing` `Field.toDivisionRing` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instLTAbs` `const` `IsAbsoluteValue.abs_isAbsoluteValue`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `lim`	—	`IsAbsoluteValue.abs_isAbsoluteValue` `const_lt` `lt_of_eq_of_lt` `equiv_lim`
`lim_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `lim` `CauSeq` `instMul` `const`	—	`lim_mul_lim` `lim_const`
`lim_mul_lim` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `lim` `CauSeq` `instMul`	—	`eq_lim_of_const_equiv` `coe_add` `sub_mul` `mul_sub` `sub_add_sub_cancel'` `add_limZero` `mul_limZero_left` `equiv_lim` `mul_limZero_right`
`lim_neg` 📖	mathematical	—	`lim` `CauSeq` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`lim_eq_of_equiv_const` `const_neg` `sub_neg_eq_add` `add_comm` `sub_eq_add_neg` `equiv_lim`
`lim_sub` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `lim` `CauSeq` `instSub`	—	`sub_eq_add_neg` `lim_neg` `lim_add`
`lt_lim` 📖	mathematical	`CauSeq` `DivisionRing.toRing` `Field.toDivisionRing` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instLTAbs` `const` `IsAbsoluteValue.abs_isAbsoluteValue`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `lim`	—	`IsAbsoluteValue.abs_isAbsoluteValue` `const_lt` `lt_of_lt_of_eq` `equiv_lim`

CauSeq.Completion

Definitions

Name	Category	Theorems
`instAddCauchy` 📖	CompOp	6 math math: `ofRat_add`, `mk_add`, `Real.cauchy_add`, `Real.ofCauchy_add`, `Real.ringEquivCauchy_apply`, `Real.ringEquivCauchy_symm_apply_cauchy`
`instDivInvMonoid` 📖	CompOp	2 math math: `ofRat_div`, `Real.ofCauchy_div`
`instInhabitedCauchy` 📖	CompOp	—
`instIntCastCauchy` 📖	CompOp	3 math math: `Real.ofCauchy_intCast`, `Real.cauchy_intCast`, `ofRat_intCast`
`instInvCauchy` 📖	CompOp	7 math math: `ofRat_inv`, `Real.cauchy_inv`, `inv_mk`, `inv_zero`, `mul_inv_cancel`, `inv_mul_cancel`, `Real.ofCauchy_inv`
`instMulCauchy` 📖	CompOp	8 math math: `ofRat_mul`, `Real.ofCauchy_mul`, `mk_mul`, `mul_inv_cancel`, `inv_mul_cancel`, `Real.cauchy_mul`, `Real.ringEquivCauchy_apply`, `Real.ringEquivCauchy_symm_apply_cauchy`
`instNNRatCast` 📖	CompOp	3 math math: `Real.ofCauchy_nnratCast`, `Real.cauchy_nnratCast`, `ofRat_nnratCast`
`instNatCastCauchy` 📖	CompOp	3 math math: `Real.ofCauchy_natCast`, `Real.cauchy_natCast`, `ofRat_natCast`
`instNegCauchy` 📖	CompOp	4 math math: `Real.cauchy_neg`, `Real.ofCauchy_neg`, `mk_neg`, `ofRat_neg`
`instOneCauchy` 📖	CompOp	5 math math: `ofRat_one`, `mul_inv_cancel`, `inv_mul_cancel`, `Real.ofCauchy_one`, `Real.cauchy_one`
`instPowCauchyNat` 📖	CompOp	1 math math: `mk_pow`
`instRatCast` 📖	CompOp	4 math math: `ofRat_ratCast`, `ofRat_rat`, `Real.ofCauchy_ratCast`, `Real.cauchy_ratCast`
`instReprCauchy` 📖	CompOp	—
`instSMulCauchyOfIsScalarTower` 📖	CompOp	1 math math: `mk_smul`
`instSubCauchy` 📖	CompOp	4 math math: `Real.cauchy_sub`, `Real.ofCauchy_sub`, `ofRat_sub`, `mk_sub`
`instZeroCauchy` 📖	CompOp	6 math math: `Real.ofCauchy_zero`, `inv_zero`, `ofRat_zero`, `Real.cauchy_zero`, `mk_eq_zero`, `PadicSeq.eq_zero_iff_equiv_zero`
`mk` 📖	CompOp	—
`ofRat` 📖	CompOp	15 math math: `ofRat_div`, `ofRat_inv`, `ofRat_mul`, `ofRat_ratCast`, `ofRat_rat`, `ofRat_one`, `ofRat_add`, `ofRat_sub`, `ofRat_nnratCast`, `ofRat_zero`, `ofRat_injective`, `ofRatRingHom_apply`, `ofRat_intCast`, `ofRat_natCast`, `ofRat_neg`
`ofRatRingHom` 📖	CompOp	1 math math: `ofRatRingHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cau_seq_zero_ne_one` 📖	mathematical	—	`CauSeq` `DivisionRing.toRing` `CauSeq.equiv` `CauSeq.instZero` `CauSeq.instOne`	—	`sub_zero` `one_ne_zero` `NeZero.one` `DivisionRing.toNontrivial` `CauSeq.const_limZero`
`inv_mk` 📖	mathematical	`CauSeq.LimZero` `DivisionRing.toRing`	`Cauchy` `instInvCauchy` `CauSeq.inv`	—	—
`inv_mul_cancel` 📖	mathematical	—	`Cauchy` `DivisionRing.toRing` `instMulCauchy` `instInvCauchy` `instOneCauchy`	—	`CauSeq.inv_mul_cancel`
`inv_zero` 📖	mathematical	—	`Cauchy` `DivisionRing.toRing` `instInvCauchy` `instZeroCauchy`	—	`CauSeq.zero_limZero`
`mk_add` 📖	mathematical	—	`Cauchy` `instAddCauchy` `CauSeq` `CauSeq.instAdd`	—	—
`mk_eq` 📖	mathematical	—	`CauSeq.LimZero` `CauSeq` `CauSeq.instSub`	—	`Quotient.eq`
`mk_eq_mk` 📖	mathematical	—	`CauSeq` `CauSeq.equiv`	—	—
`mk_eq_zero` 📖	mathematical	—	`Cauchy` `instZeroCauchy` `CauSeq.LimZero`	—	`Quotient.eq` `sub_zero`
`mk_mul` 📖	mathematical	—	`Cauchy` `instMulCauchy` `CauSeq` `CauSeq.instMul`	—	—
`mk_neg` 📖	mathematical	—	`Cauchy` `instNegCauchy` `CauSeq` `CauSeq.instNeg`	—	—
`mk_pow` 📖	mathematical	—	`Cauchy` `instPowCauchyNat` `CauSeq` `CauSeq.instPowNat`	—	—
`mk_smul` 📖	mathematical	—	`Cauchy` `instSMulCauchyOfIsScalarTower` `CauSeq` `CauSeq.instSMul`	—	—
`mk_sub` 📖	mathematical	—	`Cauchy` `instSubCauchy` `CauSeq` `CauSeq.instSub`	—	—
`mul_inv_cancel` 📖	mathematical	—	`Cauchy` `DivisionRing.toRing` `instMulCauchy` `instInvCauchy` `instOneCauchy`	—	`CauSeq.mul_inv_cancel`
`ofRatRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Cauchy` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Cauchy.ring` `RingHom.instFunLike` `ofRatRingHom` `ofRat`	—	—
`ofRat_add` 📖	mathematical	—	`ofRat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Cauchy` `instAddCauchy`	—	`CauSeq.const_add`
`ofRat_div` 📖	mathematical	—	`ofRat` `DivisionRing.toRing` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Cauchy` `instDivInvMonoid`	—	`div_eq_mul_inv` `ofRat_mul` `ofRat_inv`
`ofRat_injective` 📖	mathematical	—	`Cauchy` `ofRat`	—	—
`ofRat_intCast` 📖	mathematical	—	`ofRat` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Cauchy` `instIntCastCauchy`	—	—
`ofRat_inv` 📖	mathematical	—	`ofRat` `DivisionRing.toRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `Cauchy` `instInvCauchy`	—	`CauSeq.const.congr_simp` `CauSeq.const_limZero` `GroupWithZero.inv_zero`
`ofRat_mul` 📖	mathematical	—	`ofRat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Cauchy` `instMulCauchy`	—	`CauSeq.const_mul`
`ofRat_natCast` 📖	mathematical	—	`ofRat` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Cauchy` `instNatCastCauchy`	—	—
`ofRat_neg` 📖	mathematical	—	`ofRat` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Cauchy` `instNegCauchy`	—	`CauSeq.const_neg`
`ofRat_nnratCast` 📖	mathematical	—	`ofRat` `DivisionRing.toRing` `NNRat.cast` `DivisionRing.toNNRatCast` `Cauchy` `instNNRatCast`	—	—
`ofRat_one` 📖	mathematical	—	`ofRat` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Cauchy` `instOneCauchy`	—	—
`ofRat_ratCast` 📖	mathematical	—	`ofRat` `DivisionRing.toRing` `DivisionRing.toRatCast` `Cauchy` `instRatCast`	—	—
`ofRat_sub` 📖	mathematical	—	`ofRat` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Cauchy` `instSubCauchy`	—	`CauSeq.const_sub`
`ofRat_zero` 📖	mathematical	—	`ofRat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Cauchy` `instZeroCauchy`	—	—
`zero_ne_one` 📖	—	—	—	—	`cau_seq_zero_ne_one` `mk_eq`

CauSeq.Completion.Cauchy

Definitions

Name	Category	Theorems
`commRing` 📖	CompOp	—
`divisionRing` 📖	CompOp	5 math math: `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply`, `Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn`, `PadicInt.coe_adicCompletionIntegersEquiv_symm_apply`, `PadicInt.coe_adicCompletionIntegersEquiv_apply`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonTrivial` 📖	mathematical	—	`Nontrivial` `CauSeq.Completion.Cauchy`	—	`Function.Injective.nontrivial` `CauSeq.Completion.ofRat_injective`

CauSeq.IsComplete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isComplete` 📖	mathematical	—	`CauSeq` `CauSeq.equiv` `CauSeq.const`	—	—

---

← Back to Index