Theorems · Definition · commutative algebra
smoothingSeminorm
{R : Type u_1} → [inst : CommRing R] → (μ : RingSeminorm R) → μ 1 ≤ 1 → IsNonarchimedean ⇑μ → RingSeminorm RIf μ 1 ≤ 1 and μ is nonarchimedean, then smoothingFun is a ring seminorm.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 211 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement · cited by 25,697
- CommRingstatement and proof · cited by 17,173
- IsNonarchimedeanstatement and proof · cited by 77
- RingSeminormstatement and proof · cited by 58
- smoothingFunproof · cited by 13
Cited by5
Results whose statement or proof uses this declaration.
- exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensionalproof · cited by 5
- smoothingSeminorm_apply_of_map_mul_eq_mulstatement · cited by 1
- smoothingSeminorm_of_mulstatement · cited by 1
- smoothingSeminorm_map_one_le_onestatement · cited by 0
- smoothingSeminorm.congr_simpstatement and proof · cited by 0