Mathlib Map

Theorems · Definition · commutative algebra

WithIdeal.i

{R : Type u_2} → {inst : CommRing R} → [self : WithIdeal R] → Ideal R
Defined in
Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Cited by
3 results in Mathlib
Foundations
Depth 15 from the axioms · uses no axioms
Assumes
WithIdeal
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

WithIdeal.uniformEquiv · cited by 3WithIdeal.uniformEquivWithIdeal.uniformEquiv.congr_simp · cited by 0uniformEquiv.congr_simpWithIdeal.isTopologicallyNilpotent_of_mem · cited by 0WithIdeal.isTopologically…WithIdeal.topologicalSpaceModule · cited by 0WithIdeal.topologicalSpac…WithIdeal.uniformContinuous_of_map_le · cited by 0WithIdeal.uniformContinuo…CommRing · cited by 17173CommRingIdeal · cited by 4748IdealWithIdeal · cited by 5WithIdealWithIdeal.iCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • CommRingstatement and proof · cited by 17,173
  • Idealstatement · cited by 4,748
  • WithIdealstatement and proof · cited by 5

Cited by5

Results whose statement or proof uses this declaration.