Theorems · Definition · commutative algebra
MulRingNorm.toMulRingSeminorm
{R : Type u_2} → [inst : NonAssocRing R] → MulRingNorm R → MulRingSeminorm R- Cited by
- 9 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- NonAssocRing
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.
- NonAssocRingstatement and proof · cited by 483
- MulRingNormstatement and proof · cited by 16
- MulRingSeminormstatement · cited by 12
Cited by18
Results whose statement or proof uses this declaration.
- MulRingNorm.mulRingNormEquivAbsoluteValueproof · cited by 4
- MulAlgebraNorm.extends_norm'proof · cited by 1
- MulAlgebraNorm.mk.injstatement and proof · cited by 1
- MulAlgebraNorm.mk.noConfusionstatement and proof · cited by 1
- MulAlgebraNorm.smul'statement · cited by 1
- MulAlgebraNorm.toFun_eq_coestatement · cited by 1
- MulRingNorm.eq_zero_of_map_eq_zero'statement · cited by 1
- MulAlgebraNorm.toAlgebraNormproof · cited by 1
- spectralNorm_unique_field_norm_extproof · cited by 0
- MulAlgebraNorm.casesOnstatement and proof · cited by 0
- MulAlgebraNorm.mk.injEqstatement and proof · cited by 0
- MulAlgebraNorm.mk.sizeOf_specstatement and proof · cited by 0