Structures · Algebra
MulActionWithZero
An action of a monoid with zero M₀ on a Type A, also with 0, extends MulAction and
is compatible with 0 (both in M₀ and in A), with 1 ∈ M₀, and with associativity of
multiplication on the monoid A.
- Shape
- 2 explicit arguments · adds smul_zero, zero_smul
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- Subtype
- OrderDual
- ULift
- MulOpposite
- Lex
How is a type an instance?
Loading the hierarchy index…
Assumed by108
- Polynomial.smeval
- Module.subsingleton
- Module.nontrivial
- MeasureTheory.MemLp.smul
- Polynomial.smeval_monomial
- Polynomial.smeval_X
- MeasureTheory.MemLp.const_smul
- Polynomial.smeval_one
- Polynomial.smul_pow
- Polynomial.smeval_eq_sum
- left_mem_segment
- Polynomial.smeval_C
- gauge_smul_of_nonneg
- right_mem_segment
- MeasureTheory.integrable_smul_iff
- MeasureTheory.eLpNorm_smul_le_mul_eLpNorm
- smul_inv₀
- IsNilpotent.smul
- Real.sInf_smul_of_nonneg
- MulActionWithZero.subsingleton
- IsUnit.integrable_smul_iff
- MeasureTheory.eLpNorm_const_smul_le
- MulActionWithZero.nontrivial
- IsSMulRegular.not_zero
- MulActionWithZero.zero_smul
- MeasureTheory.Lp.coeFn_lpSMul
- Bornology.IsVonNBounded.restrict_scalars
- Polynomial.smeval_zero
- IsSMulRegular.zero_iff_subsingleton
- isClosedMap_smul₀
- Polynomial.smeval_def
- bddBelow_smul_iff_of_pos
- Filter.top_smul_nhds_zero
- gauge_smul_left
- MeasureTheory.hasFiniteIntegral_smul_iff
- smul_ceilDiv
- gauge_smul_left_of_nonneg
- ContinuousMap.exists_finite_sum_smul_approximation_of_mem_uniformity
- IsSMulRegular.zero
- MeasurableSet.const_smul₀
- cardinal_eq_of_isOpen
- MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top
- MeasureTheory.eLpNorm'_const_smul_le
- LaurentPolynomial.smeval_T_pow
- closure_smul₀
- Real.smul_iSup_of_nonneg
- smulMonoidWithZeroHom
- cardinal_eq_of_mem_nhds_zero
- Set.univ_smul_nhds_zero
- bddAbove_smul_iff_of_pos