Theorems · Definition · commutative algebra
SeminormedRing.toRingSeminorm
(R : Type u_2) → [inst : SeminormedRing R] → RingSeminorm R
The seminorm on a SeminormedRing, as a RingSeminorm.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SeminormedRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Norm.normproof · cited by 5,413
- SeminormedRingstatement and proof · cited by 446
- RingSeminormstatement · cited by 58
- SeminormedRing.norm_mul_leproof · cited by 0
Cited by11
Results whose statement or proof uses this declaration.
- Polynomial.supNormproof · cited by 13
- Polynomial.exists_eq_supNormproof · cited by 2
- Polynomial.le_supNormproof · cited by 2
- Polynomial.supNorm_monomialproof · cited by 1
- Polynomial.supNorm_nonnegproof · cited by 1
- Polynomial.supNorm_zeroproof · cited by 1
- SeminormedRing.toRingSeminorm_applystatement · cited by 0
- Polynomial.supNorm_Cproof · cited by 0
- Polynomial.supNorm_def'proof · cited by 0
- Polynomial.supNorm_eq_zero_iffproof · cited by 0
- contraction_of_isPowMulproof · cited by 0