Theorems · Definition · commutative algebra
NormedField.toMulRingNorm
(R : Type u_2) → [inst : NormedField R] → MulRingNorm R
The norm on a NormedField, as a MulRingNorm.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Norm.normproof · cited by 5,413
- NormedFieldstatement and proof · cited by 1,084
- MulRingNormstatement · cited by 16
Cited by3
Results whose statement or proof uses this declaration.
- NormedAlgebra.toMulAlgebraNormproof · cited by 2
- Module.Basis.norm_mul_le_const_mul_normproof · cited by 1
- Polynomial.exists_roots_norm_sub_lt_of_norm_coeff_sub_ltproof · cited by 1