Documentation Verification Report

WithAbs

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

Statistics

Metric	Count
Definitions `semialgHomOfComp`, `instAlgebraReal_fLT`, `instAlgebraReal_fLT_1`, `instField_fLT`	4
Theorems `isometry_semiAlgHomOfComp`, `semiAlgHomOfComp_dist_eq`, `semialgHomOfComp_coe`, `instFiniteDimensional_fLT`, `instIsScalarTowerReal_fLT`, `instIsSeparable_fLT`, `instNumberFieldReal_fLT`, `instUniformContinuousConstSMulReal_fLT`, `norm_eq_abs`, `uniformContinuous_algebraMap`	10
Total	14

AbsoluteValue.Completion

Definitions

Name	Category	Theorems
`semialgHomOfComp` 📖	CompOp	3 math math: `semiAlgHomOfComp_dist_eq`, `isometry_semiAlgHomOfComp`, `semialgHomOfComp_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isometry_semiAlgHomOfComp` 📖	mathematical	`WithAbs.instAlgebraReal_fLT`	`SemialgHom` `WithAbs.instAlgebraReal_fLT_1` `WithAbs.instUniformContinuousConstSMulReal_fLT` `instFunLike` `semialgHomOfComp`	—	`WithAbs.instUniformContinuousConstSMulReal_fLT` `semiAlgHomOfComp_dist_eq`
`semiAlgHomOfComp_dist_eq` 📖	mathematical	`WithAbs.instAlgebraReal_fLT`	`SemialgHom` `WithAbs.instAlgebraReal_fLT_1` `WithAbs.instUniformContinuousConstSMulReal_fLT` `instFunLike` `semialgHomOfComp`	—	`WithAbs.instUniformContinuousConstSMulReal_fLT` `semialgHomOfComp_coe`
`semialgHomOfComp_coe` 📖	mathematical	`WithAbs.instAlgebraReal_fLT`	`SemialgHom` `WithAbs.instAlgebraReal_fLT_1` `WithAbs.instUniformContinuousConstSMulReal_fLT` `instFunLike` `semialgHomOfComp`	—	`UniformSpace.Completion.mapSemialgHom_coe`

WithAbs

Definitions

Name	Category	Theorems
`instAlgebraReal_fLT` 📖	CompOp	4 math math: `NumberField.InfinitePlace.Completion.piEquiv_smul`, `NumberField.InfinitePlace.Completion.baseChangeEquiv_tmul`, `NumberField.InfinitePlace.Completion.comapHom_cont`, `NumberField.InfinitePlace.Completion.piExtension_apply`
`instAlgebraReal_fLT_1` 📖	CompOp	5 math math: `instIsScalarTowerReal_fLT`, `AbsoluteValue.Completion.semiAlgHomOfComp_dist_eq`, `instUniformContinuousConstSMulReal_fLT`, `AbsoluteValue.Completion.isometry_semiAlgHomOfComp`, `AbsoluteValue.Completion.semialgHomOfComp_coe`
`instField_fLT` 📖	CompOp	2 math math: `instNumberFieldReal_fLT`, `instFiniteDimensional_fLT`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteDimensional_fLT` 📖	mathematical	—	`instField_fLT`	—	—
`instIsScalarTowerReal_fLT` 📖	mathematical	—	`instAlgebraReal_fLT_1`	—	—
`instIsSeparable_fLT` 📖	—	—	—	—	—
`instNumberFieldReal_fLT` 📖	mathematical	—	`instField_fLT`	—	—
`instUniformContinuousConstSMulReal_fLT` 📖	mathematical	—	`instAlgebraReal_fLT_1`	—	—
`norm_eq_abs` 📖	—	—	—	—	—
`uniformContinuous_algebraMap` 📖	—	`instAlgebraReal_fLT`	—	—	—

---

← Back to Index