Theorems · Theorem · functional analysis

WeakDual.gelfandTransform.congr_simp

∀ (𝕜 : Type u_1) (A : Type u_2) [inst : CommRing 𝕜] [inst_1 : NoZeroDivisors 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : IsTopologicalRing 𝕜] [inst_4 : TopologicalSpace A] [inst_5 : Semiring A] [inst_6 : Algebra 𝕜 A],
  WeakDual.gelfandTransform 𝕜 A = WeakDual.gelfandTransform 𝕜 A

Defined in: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Cited by: 0 results in Mathlib
Foundations: Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing NoZeroDivisors TopologicalSpace IsTopologicalRing TopologicalSpace Semiring Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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

Setstatement · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
CommRingstatement and proof · cited by 17,173
Semiringstatement and proof · cited by 13,802
Algebrastatement and proof · cited by 11,388
Set.Elemstatement · cited by 7,166
AlgHomstatement · cited by 3,236
ContinuousMapstatement · cited by 2,491
NoZeroDivisorsstatement and proof · cited by 545
IsTopologicalRingstatement and proof · cited by 402
WeakDualstatement · cited by 103
WeakDual.characterSpacestatement · cited by 39

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.