Documentation Verification Report

WithAbs

📁 Source: Mathlib/Analysis/Normed/Ring/WithAbs.lean

Statistics

Metric	Count
Definitions `LiesOver`, `WithAbs`, `algEquiv`, `equiv`, `equivWithAbs`, `instAlgebra_left`, `instAlgebra_right`, `instCommRing`, `instCommSemiring`, `instInhabited`, `instModule_left`, `instModule_right`, `instRing`, `instSemiring`, `instUnique`, `normedRing`	16
Theorems `comp_eq`, `comp_eq'`, `algebraMap_left_apply`, `algebraMap_right_apply`, `equivWithAbs_equiv_symm_apply`, `equivWithAbs_symm`, `equivWithAbs_symm_equiv_symm_apply`, `equiv_algebraMap_apply`, `equiv_equivWithAbs_symm_apply`, `instNontrivial`, `norm_eq_abv`	11
Total	27

AbsoluteValue

Definitions

Name	Category	Theorems
`LiesOver` 📖	CompData	—

AbsoluteValue.LiesOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq` 📖	mathematical	—	`AbsoluteValue.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `RingHom.injective` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Semiring.toNonAssocSemiring`	—	`comp_eq'`
`comp_eq'` 📖	mathematical	—	`AbsoluteValue.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `RingHom.injective` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Semiring.toNonAssocSemiring`	—	—

WithAbs

Definitions

Name	Category	Theorems
`algEquiv` 📖	CompOp	—
`equiv` 📖	CompOp	12 math math: `algebraMap_left_apply`, `NumberField.InfinitePlace.isometry_embedding`, `NumberField.InfinitePlace.Completion.norm_coe`, `equiv_algebraMap_apply`, `tendsto_one_div_one_add_pow_nhds_one`, `algebraMap_right_apply`, `norm_eq_abv`, `equivWithAbs_equiv_symm_apply`, `NumberField.InfinitePlace.isometry_embedding_of_isReal`, `equiv_equivWithAbs_symm_apply`, `NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv`, `equivWithAbs_symm_equiv_symm_apply`
`equivWithAbs` 📖	CompOp	7 math math: `AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs`, `AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zero`, `equivWithAbs_equiv_symm_apply`, `equiv_equivWithAbs_symm_apply`, `equivWithAbs_symm`, `AbsoluteValue.isEquiv_iff_isHomeomorph`, `equivWithAbs_symm_equiv_symm_apply`
`instAlgebra_left` 📖	CompOp	3 math math: `algebraMap_left_apply`, `equiv_algebraMap_apply`, `instIsSeparable`
`instAlgebra_right` 📖	CompOp	3 math math: `equiv_algebraMap_apply`, `algebraMap_right_apply`, `NumberField.InfinitePlace.denseRange_algebraMap_pi`
`instCommRing` 📖	CompOp	1 math math: `instIsSeparable`
`instCommSemiring` 📖	CompOp	2 math math: `algebraMap_left_apply`, `equiv_algebraMap_apply`
`instInhabited` 📖	CompOp	—
`instModule_left` 📖	CompOp	1 math math: `instFiniteDimensional`
`instModule_right` 📖	CompOp	—
`instRing` 📖	CompOp	5 math math: `tendsto_one_div_one_add_pow_nhds_one`, `AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp`, `AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp`, `AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp`, `AbsoluteValue.Completion.extensionEmbedding_of_comp_coe`
`instSemiring` 📖	CompOp	17 math math: `AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs`, `algebraMap_left_apply`, `NumberField.InfinitePlace.isometry_embedding`, `NumberField.InfinitePlace.Completion.norm_coe`, `equiv_algebraMap_apply`, `tendsto_one_div_one_add_pow_nhds_one`, `algebraMap_right_apply`, `AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zero`, `norm_eq_abv`, `NumberField.InfinitePlace.denseRange_algebraMap_pi`, `equivWithAbs_equiv_symm_apply`, `NumberField.InfinitePlace.isometry_embedding_of_isReal`, `equiv_equivWithAbs_symm_apply`, `equivWithAbs_symm`, `NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv`, `AbsoluteValue.isEquiv_iff_isHomeomorph`, `equivWithAbs_symm_equiv_symm_apply`
`instUnique` 📖	CompOp	—
`normedRing` 📖	CompOp	1 math math: `norm_eq_abv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_left_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WithAbs` `CommSemiring.toSemiring` `Semiring.toNonAssocSemiring` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra_left` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv`	—	—
`algebraMap_right_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WithAbs` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra_right` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv`	—	—
`equivWithAbs_equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equivWithAbs` `RingEquiv.symm` `equiv`	—	—
`equivWithAbs_symm` 📖	mathematical	—	`RingEquiv.symm` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `equivWithAbs`	—	—
`equivWithAbs_symm_equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `equivWithAbs` `equiv`	—	—
`equiv_algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv` `RingHom` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra_left` `instAlgebra_right`	—	—
`equiv_equivWithAbs_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WithAbs` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv` `RingEquiv.symm` `equivWithAbs`	—	—
`instNontrivial` 📖	mathematical	—	`Nontrivial` `WithAbs`	—	—
`norm_eq_abv` 📖	mathematical	—	`Norm.norm` `WithAbs` `Real` `Real.semiring` `Real.partialOrder` `Ring.toSemiring` `NormedRing.toNorm` `normedRing` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv`	—	—

(root)

Definitions

Name	Category	Theorems
`WithAbs` 📖	CompOp	29 math math: `AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs`, `NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal`, `WithAbs.algebraMap_left_apply`, `NumberField.InfinitePlace.isometry_embedding`, `NumberField.InfiniteAdeleRing.algebraMap_apply`, `NumberField.InfinitePlace.Completion.norm_coe`, `WithAbs.equiv_algebraMap_apply`, `NumberField.InfinitePlace.Completion.isometry_extensionEmbedding`, `WithAbs.tendsto_one_div_one_add_pow_nhds_one`, `NumberField.InfinitePlace.Completion.locallyCompactSpace`, `WithAbs.algebraMap_right_apply`, `NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe`, `WithAbs.instFiniteDimensional`, `WithAbs.norm_eq_abv`, `NumberField.InfinitePlace.Completion.extensionEmbedding_coe`, `NumberField.InfinitePlace.denseRange_algebraMap_pi`, `WithAbs.equivWithAbs_equiv_symm_apply`, `NumberField.InfinitePlace.isometry_embedding_of_isReal`, `WithAbs.equiv_equivWithAbs_symm_apply`, `NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal_coe`, `WithAbs.equivWithAbs_symm`, `NumberField.AdeleRing.algebraMap_fst_apply`, `WithAbs.instNontrivial`, `NumberField.InfinitePlace.Completion.isometry_extensionEmbedding_of_isReal`, `NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv`, `WithAbs.instIsSeparable`, `NumberField.InfinitePlace.Completion.Rat.norm_infinitePlace_completion`, `AbsoluteValue.isEquiv_iff_isHomeomorph`, `WithAbs.equivWithAbs_symm_equiv_symm_apply`

---

← Back to Index