Theorems · Theorem · number theory

CovBySMul.trans

∀ {M : Type u_1} {N : Type u_2} {X : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : MulAction M X]
  [inst_3 : MulAction N X] {K L : ℝ} {A B C : Set X} [inst_4 : SMul M N] [IsScalarTower M N X],
  CovBySMul M K A B → CovBySMul N L B C → CovBySMul N (K * L) A C

Defined in

Mathlib.Combinatorics.Additive.CovBySMul

Cited by

2 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidMonoidMulActionMulActionSMulIsScalarTower