Commit 2023-06-02 10:22 488dc767

View on Github →

feat: port Analysis.VonNeumannAlgebra.Basic (#4569)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/VonNeumannAlgebra/Basic.lean

added theorem VonNeumannAlgebra.centralizer_centralizer

added theorem VonNeumannAlgebra.coe_commutant

added def VonNeumannAlgebra.commutant

added theorem VonNeumannAlgebra.commutant_commutant

added theorem VonNeumannAlgebra.ext

added theorem VonNeumannAlgebra.mem_carrier

added theorem VonNeumannAlgebra.mem_commutant_iff

added structure VonNeumannAlgebra