Theorems · Definition · commutative algebra
MvPowerSeries.IsRestricted.subring
{R : Type u_1} → [inst : NormedRing R] → {σ : Type u_2} → [IsUltrametricDist R] → (σ → ℝ) → Subring (MvPowerSeries σ R)Restricted power series as a subring of MvPowerSeries σ R.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedRingIsUltrametricDist
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- AddSubgroupproof · cited by 3,232
- NormedRingstatement and proof · cited by 924
- MvPowerSeriesstatement and proof · cited by 659
- Subringstatement · cited by 602
- AddSubmonoid.toAddSubsemigroupproof · cited by 198
- AddSubsemigroup.carrierproof · cited by 198
- IsUltrametricDiststatement and proof · cited by 177
- AddSubgroup.toAddSubmonoidproof · cited by 91
- MvPowerSeries.isRestricted.mulproof · cited by 1
- MvPowerSeries.isRestricted_oneproof · cited by 0
- MvPowerSeries.IsRestricted.addSubgroupproof · cited by 0
Cited by1
Results whose statement or proof uses this declaration.
- PowerSeries.IsRestricted.subringproof · cited by 0