Theorems · Theorem · number theory

IsDivSequence.smul

Deprecated since 2026-06-30Use IsDvdSequence.smul instead.

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Dvd α] [inst_1 : Monoid β] [inst_2 : Monoid γ] {f : α → γ}
  [inst_3 : SMul β γ] [IsScalarTower β γ γ] [IsScalarTower β β γ] [SMulCommClass β γ γ] (b : β),
  IsDvdSequence f → IsDvdSequence (b • f)

Alias of IsDvdSequence.smul.

Defined in

Mathlib.Data.Nat.DvdSequence

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext, Quot.sound

Assumes

DvdMonoidMonoidSMulIsScalarTowerIsScalarTowerSMulCommClass