Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-13 13:32 7d34f786

View on Github →

chore(algebra/algebra/subalgebra): reduce imports (#12636) Splitting a file, and reducing imports. No change in contents.

Estimated changes

Renamed src/algebra/algebra/subalgebra.lean to src/algebra/algebra/subalgebra/basic.lean

deleted theorem subalgebra.coe_pointwise_smul

deleted theorem subalgebra.mul_self

deleted theorem subalgebra.pointwise_smul_to_submodule

deleted theorem subalgebra.pointwise_smul_to_subring

deleted theorem subalgebra.pointwise_smul_to_subsemiring

deleted theorem subalgebra.smul_mem_pointwise_smul

Created src/algebra/algebra/subalgebra/pointwise.lean

added theorem subalgebra.coe_pointwise_smul

added theorem subalgebra.mul_self

added theorem subalgebra.pointwise_smul_to_submodule

added theorem subalgebra.pointwise_smul_to_subring

added theorem subalgebra.pointwise_smul_to_subsemiring

added theorem subalgebra.smul_mem_pointwise_smul

Modified src/algebra/algebra/tower.lean

Modified src/algebra/category/Algebra/basic.lean

Modified src/algebra/direct_sum/internal.lean

Modified src/algebra/free_algebra.lean

Modified src/algebra/lie/of_associative.lean

Modified src/linear_algebra/finite_dimensional.lean

Modified src/linear_algebra/tensor_algebra/basic.lean

Modified src/ring_theory/adjoin/basic.lean

Modified src/ring_theory/dedekind_domain/ideal.lean

Modified src/ring_theory/polynomial/symmetric.lean

Modified src/topology/algebra/algebra.lean

Modified src/topology/continuous_function/algebra.lean