Mathlib Map

Theorems · Theorem · number theory

AbstractMeasure.prodMk.congr_simp

∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : LocallyCompactSpace X]
  [inst_6 : LocallyCompactSpace Y], AbstractMeasure.prodMk = AbstractMeasure.prodMk
Defined in
Mathlib.NumberTheory.Padics.Measure.Basic
Cited by
0 results in Mathlib
Foundations
Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpaceTopologicalSpaceCommRingTopologicalSpaceIsTopologicalRingLocallyCompactSpaceLocallyCompactSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

TopologicalSpace · cited by 24529TopologicalSpaceRingHom.id · cited by 18349RingHom.idCommRing · cited by 17173CommRingLinearMap · cited by 10215LinearMapIsTopologicalRing · cited by 402IsTopologicalRingLocallyCompactSpace · cited by 324LocallyCompactSpaceAbstractMeasure · cited by 20AbstractMeasureAbstractMeasure.prodMk · cited by 5AbstractMeasure.prodMkprodMk.congr_simpCITED BYCITES

Cites8

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

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.