Theorem Subalgebra.mul_toSubmodule

Modification history

2023-08-10 19:52

Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Subalgebra.mul_toSubmodule View on Github →

2023-03-15 22:32

Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

feat: port Algebra.Algebra.Subalgebra.Pointwise (#2913)

Added Subalgebra.mul_toSubmodule View on Github →