SMulCommClass R₁ R R implies IsScalarTower R₁ R R

Stream: Is there code for X?

[Kenny Lau]

I'm too deep in this generalised nonsense, I have no idea what I'm proving mathematically anymore, but I did stumble on this theorem that seems to not be in Mathlib:

import Mathlib

universe u v

variable (R₁ : Type u) (R : Type v)
  [Monoid R₁] [CommSemiring R] [DistribMulAction R₁ R] [SMulCommClass R₁ R R]

theorem isScalarTower_of_commSemiring_of_smulCommClass : IsScalarTower R₁ R R := by
  fail_if_success exact?
  exact ⟨fun x₁ y z ↦ by rw [smul_eq_mul, mul_comm, ← smul_eq_mul, ← smul_comm, smul_eq_mul,
    mul_comm, ← smul_eq_mul]⟩

[Kenny Lau]

The converse is docs#SMulCommClass.of_commMonoid

[Kenny Lau]

oh and of course I don't need the addition at all:

import Mathlib

universe u v

variable (R₁ : Type u) (R : Type v)
  [Monoid R₁] [CommMonoid R] [MulAction R₁ R]

theorem isScalarTower_of_commSemiring_of_smulCommClass [SMulCommClass R₁ R R] : IsScalarTower R₁ R R := by
  fail_if_success exact?
  exact ⟨fun x₁ y z ↦ by rw [smul_eq_mul, mul_comm, ← smul_eq_mul, ← smul_comm, smul_eq_mul,
    mul_comm, ← smul_eq_mul]⟩

theorem smulCommClass_of_commSemiring_of_isScalarTower [IsScalarTower R₁ R R] : SMulCommClass R₁ R R := by
  exact SMulCommClass.of_commMonoid R₁ R R

[Kenny Lau]

@Yaël Dillies do we want this?

[Eric Wieser]

I think it's harmless as a theorem but would be a bad instance

[Yaël Dillies]

Probably not as an instance for performance

[Eric Wieser]

I guess you could even add an Iff version to show that the two are equivalent

[Kenny Lau]

@Eric Wieser @Yaël Dillies #26948 created