Structures · Algebra
SMulZeroClass
Typeclass for scalar multiplication that preserves 0 on the right.
- Shape
- 2 explicit arguments · adds smul_zero
Extends1
Extended by2
Concrete types that are instances6
- HahnSeries
- DomMulAct
- Units
- OrderDual
- ULift
- PUnit
How is a type an instance?
Loading the hierarchy index…
Assumed by288
- smul_zero
- Finsupp.smul_single
- Polynomial.coeff_smul
- norm_smul_le
- MeasureTheory.Integrable.smul
- smul_nonneg
- Polynomial.eval_smul
- nnnorm_smul_le
- MonoidAlgebra.smul_single
- SkewMonoidAlgebra.coeff_mul
- AddMonoidAlgebra.smul_single
- Polynomial.smul_C
- Unitization.inr_smul
- Finsupp.support_smul
- right_ne_zero_of_smul
- SkewMonoidAlgebra.smul_single
- Finsupp.sum_smul_index'
- Function.support_smul_subset_right
- SkewMonoidAlgebra.coeff_smul
- Polynomial.degree_smul_le
- Polynomial.natDegree_smul_le
- smul_pos
- lipschitzWith_smul
- Matrix.smul_single
- cfcₙ_smul
- IsSMulRegular.right_eq_zero_of_smul
- Polynomial.smul_monomial
- zero_ceilDiv
- smul_eq_zero_of_right
- cfc_smul_id
- DFinsupp.smul_apply
- MeasureTheory.HasFiniteIntegral.smul
- zero_floorDiv
- IntervalIntegrable.smul
- cfc_smul
- MvPolynomial.smul_monomial
- HahnSeries.coeff_smul
- ceilDiv_le_iff_le_smul
- Set.indicator_smul_apply
- smul_nonpos_of_nonneg_of_nonpos
- Finsupp.smul_apply
- cfc_comp_smul
- floorDiv_of_nonpos
- Polynomial.leadingCoeff_smul_of_smul_regular
- Mathlib.Meta.Positivity.smul_nonneg_of_pos_of_nonneg
- ceilDiv_of_nonpos
- le_floorDiv_iff_smul_le
- MeasureTheory.IntegrableAtFilter.smul
- gc_floorDiv_smul
- tsupport_smul_subset_right