Commit 2025-01-10 18:59 111b4c03

View on Github →

feat: product of subalgebras (#20202) From FLT

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Subalgebra/Pi.lean

added theorem Subalgebra.mem_pi

added def Subalgebra.pi

added theorem Subalgebra.pi_mono

added theorem Subalgebra.pi_toSubmodule

added theorem Subalgebra.pi_top

Modified Mathlib/Algebra/Group/Subgroup/Defs.lean

deleted theorem Subgroup.coe_copy

Modified Mathlib/Algebra/Module/Submodule/Defs.lean

Modified Mathlib/LinearAlgebra/Pi.lean

deleted theorem Submodule.coe_pi