Loogle!

Result

Found 20 declarations whose name contains "neumann".

• VonNeumannAlgebra 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Type u
• VonNeumannAlgebra.commutant 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : VonNeumannAlgebra H) : VonNeumannAlgebra H
• VonNeumannAlgebra.commutant_commutant 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : VonNeumannAlgebra H) : S.commutant.commutant = S
• VonNeumannAlgebra.instSetLike 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : SetLike (VonNeumannAlgebra H) (H →L[ℂ] H)
• VonNeumannAlgebra.instStarMemClass 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : StarMemClass (VonNeumannAlgebra H) (H →L[ℂ] H)
• VonNeumannAlgebra.instSubringClass 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : SubringClass (VonNeumannAlgebra H) (H →L[ℂ] H)
• VonNeumannAlgebra.commutant.eq_1 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : VonNeumannAlgebra H) : S.commutant = { toStarSubalgebra := StarSubalgebra.centralizer ℂ ↑S, centralizer_centralizer' := ⋯ }
• VonNeumannAlgebra.coe_commutant 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : VonNeumannAlgebra H) : ↑S.commutant = (↑S).centralizer
• VonNeumannAlgebra.ext 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S T : VonNeumannAlgebra H} (h : ∀ (x : H →L[ℂ] H), x ∈ S ↔ x ∈ T) : S = T
• VonNeumannAlgebra.ext_iff 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S T : VonNeumannAlgebra H} : S = T ↔ ∀ (x : H →L[ℂ] H), x ∈ S ↔ x ∈ T
• VonNeumannAlgebra.toStarSubalgebra 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (self : VonNeumannAlgebra H) : StarSubalgebra ℂ (H →L[ℂ] H)
• VonNeumannAlgebra.centralizer_centralizer 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : VonNeumannAlgebra H) : (↑S).centralizer.centralizer = ↑S
• VonNeumannAlgebra.coe_toStarSubalgebra 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : VonNeumannAlgebra H) : ↑S.toStarSubalgebra = ↑S
• VonNeumannAlgebra.mem_commutant_iff 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : VonNeumannAlgebra H} {z : H →L[ℂ] H} : z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g
• VonNeumannAlgebra.mem_carrier 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : VonNeumannAlgebra H} {x : H →L[ℂ] H} : x ∈ S.toStarSubalgebra ↔ x ∈ ↑S
• VonNeumannAlgebra.centralizer_centralizer' 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (self : VonNeumannAlgebra H) : self.carrier.centralizer.centralizer = self.carrier
• VonNeumannAlgebra.mk 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (toStarSubalgebra : StarSubalgebra ℂ (H →L[ℂ] H)) (centralizer_centralizer' : toStarSubalgebra.carrier.centralizer.centralizer = toStarSubalgebra.carrier) : VonNeumannAlgebra H
• VonNeumannAlgebra.coe_mk 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : StarSubalgebra ℂ (H →L[ℂ] H)) (h : S.carrier.centralizer.centralizer = S.carrier) : ↑{ toStarSubalgebra := S, centralizer_centralizer' := h } = ↑S
• VonNeumannAlgebra.mk.injEq 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (toStarSubalgebra : StarSubalgebra ℂ (H →L[ℂ] H)) (centralizer_centralizer' : toStarSubalgebra.carrier.centralizer.centralizer = toStarSubalgebra.carrier) (toStarSubalgebra✝ : StarSubalgebra ℂ (H →L[ℂ] H)) (centralizer_centralizer'✝ : toStarSubalgebra✝.carrier.centralizer.centralizer = toStarSubalgebra✝.carrier) : ({ toStarSubalgebra := toStarSubalgebra, centralizer_centralizer' := centralizer_centralizer' } = { toStarSubalgebra := toStarSubalgebra✝, centralizer_centralizer' := centralizer_centralizer'✝ }) = (toStarSubalgebra = toStarSubalgebra✝)
• VonNeumannAlgebra.mk.sizeOf_spec 📋 Mathlib.Analysis.VonNeumannAlgebra.Basic
  {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [SizeOf H] (toStarSubalgebra : StarSubalgebra ℂ (H →L[ℂ] H)) (centralizer_centralizer' : toStarSubalgebra.carrier.centralizer.centralizer = toStarSubalgebra.carrier) : sizeOf { toStarSubalgebra := toStarSubalgebra, centralizer_centralizer' := centralizer_centralizer' } = 1 + sizeOf toStarSubalgebra + sizeOf centralizer_centralizer'

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision f167e8d