Commit 2023-03-15 22:32 7fb7eebe

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

added theorem Subalgebra.coe_pointwise_smul

added theorem Subalgebra.mul_self

added theorem Subalgebra.mul_toSubmodule

added theorem Subalgebra.mul_toSubmodule_le

added theorem Subalgebra.pointwise_smul_toSubmodule

added theorem Subalgebra.pointwise_smul_toSubring

added theorem Subalgebra.pointwise_smul_toSubsemiring

added theorem Subalgebra.smul_mem_pointwise_smul