Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-27 19:56 e5cd2ea1

View on Github →

feat(analysis/von_neumann): concrete and abstract definitions of a von Neumann algebra (#12329)

Estimated changes

Modified src/algebra/algebra/subalgebra/basic.lean

added theorem set.algebra_map_mem_centralizer

added def subalgebra.centralizer

added theorem subalgebra.centralizer_le

added theorem subalgebra.centralizer_univ

added theorem subalgebra.coe_centralizer

added theorem subalgebra.mem_centralizer_iff

Created src/algebra/star/subalgebra.lean

added def star_subalgebra.centralizer

added theorem star_subalgebra.centralizer_le

added theorem star_subalgebra.coe_centralizer

added theorem star_subalgebra.mem_centralizer_iff

added structure star_subalgebra

Modified src/analysis/inner_product_space/adjoint.lean

Created src/analysis/von_neumann_algebra/basic.lean

added structure von_neumann_algebra

Modified src/group_theory/submonoid/basic.lean

Modified src/group_theory/submonoid/centralizer.lean

added theorem submonoid.centralizer_le

deleted theorem submonoid.centralizer_subset

modified theorem submonoid.coe_centralizer

Modified src/ring_theory/subsemiring/basic.lean

added def subsemiring.centralizer

added theorem subsemiring.centralizer_le

added theorem subsemiring.centralizer_to_submonoid

added theorem subsemiring.centralizer_univ

added theorem subsemiring.coe_centralizer

added theorem subsemiring.mem_centralizer_iff