Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-30 19:45 806bbb01

View on Github →

refactor(algebra/group/defs): rename has_scalar to has_smul (#14559) Discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/scalar.20smul.20naming.20discrepancy

Estimated changes

modified theorem alg_hom.map_smul_of_tower
modified theorem subalgebra.coe_algebra_map
modified theorem subalgebra.coe_smul
modified theorem subalgebra.smul_def
modified theorem unitization.coe_smul
modified theorem unitization.fst_mul
modified theorem unitization.fst_smul
modified theorem unitization.inl_smul
modified theorem unitization.snd_mul
modified theorem unitization.snd_smul
modified theorem units.smul_mk0
modified structure module.core
modified theorem is_smul_regular.pi
modified theorem smul_pi_subset
modified theorem smul_univ_pi
modified theorem submodule.coe_smul_of_tower
modified theorem submodule.smul_mem_iff'
modified theorem submodule.smul_of_tower_mem
modified def module.is_torsion'
modified theorem ulift.smul_down'
modified theorem ulift.smul_down
modified theorem mul_opposite.op_smul
modified theorem mul_opposite.unop_smul
modified theorem antitone_smul_left
modified theorem strict_anti_smul_left
modified theorem monotone_smul_left
modified theorem order_dual.of_dual_smul
modified theorem order_dual.to_dual_smul
modified theorem strict_mono_smul_left
modified theorem function.periodic.smul
modified def is_smul_regular
modified theorem self_adjoint.coe_smul
modified theorem self_adjoint.smul_mem
modified theorem sym_alg.sym_smul
modified theorem sym_alg.unsym_smul
modified theorem triv_sq_zero_ext.fst_mul
modified theorem triv_sq_zero_ext.fst_smul
modified theorem triv_sq_zero_ext.inl_smul
modified theorem triv_sq_zero_ext.inr_smul
modified theorem triv_sq_zero_ext.snd_mul
modified theorem triv_sq_zero_ext.snd_smul
modified theorem tropical.trop_smul
modified theorem tropical.untrop_pow
modified structure convex_cone
modified theorem add_group_seminorm.coe_smul
modified theorem add_group_seminorm.smul_sup
modified theorem seminorm.coe_smul
modified theorem seminorm.smul_apply
modified theorem seminorm.smul_inf
modified theorem seminorm.smul_sup
modified structure seminorm
modified theorem is_smul_regular.matrix
modified theorem matrix.col_smul
modified theorem matrix.conj_transpose_smul
modified theorem matrix.diag_smul
modified theorem matrix.map_smul
modified theorem matrix.minor_smul
modified theorem matrix.row_smul
modified theorem matrix.transpose_smul
modified theorem matrix.from_blocks_smul
modified theorem matrix.hadamard_smul
modified theorem matrix.smul_hadamard
modified theorem matrix.smul_vec2
modified theorem matrix.smul_vec3
modified theorem ennreal.coe_smul
modified theorem set.image2_smul
modified theorem set.range_smul_range
modified theorem set.smul_set_range
modified theorem intermediate_field.coe_smul
deleted def has_scalar.comp
added def has_smul.comp
modified theorem mul_smul_comm
modified theorem smul_assoc
modified theorem smul_comm_class.symm
modified theorem smul_left_injective'
modified theorem smul_mul_assoc
modified theorem smul_one_mul
modified theorem smul_one_smul
modified theorem smul_smul_smul_comm
modified theorem function.extend_smul
modified theorem function.update_smul
modified theorem pi.smul_apply'
modified theorem pi.smul_apply
modified theorem pi.smul_def
modified theorem set.piecewise_smul
modified structure sub_mul_action
modified theorem units.smul_def
modified theorem units.smul_is_unit
modified theorem localization.smul_mk
modified theorem submonoid.smul_def
modified theorem matrix.circulant_smul
modified theorem matrix.is_symm.smul
modified theorem submodule.span_subset_span
modified theorem tensor_product.smul.aux_of
modified theorem equiv.smul_def
modified theorem filter.eventually_eq.smul
modified theorem filter.germ.coe_smul'
modified theorem filter.germ.coe_smul
modified theorem measure_theory.adapted.smul
modified theorem polynomial_smul_apply
modified theorem subring.smul_def
modified theorem subsemiring.smul_def
modified theorem continuous_map.coe_smul
modified theorem continuous_map.smul_apply
modified theorem continuous_map.smul_comp
modified theorem locally_constant.coe_smul
modified theorem locally_constant.smul_apply
modified def foo