Theorems / mh_alge_1c5663

Mathlib held-out

Algebra · medium

Statement, exactly as the model and Lean see it
theorem lg_target {α : Type u_1} {G₀ : Type u_2} [GroupWithZero G₀] [SMul α G₀] [SMulCommClass G₀ α G₀] [IsScalarTower α G₀ G₀] : SMulCommClass (ConjAct G₀) α G₀ := by
Mathlib declaration
ConjAct.smulCommClass₀'
Held-out module
Mathlib.Algebra.GroupWithZero.Action.ConjAct
Banned modules (itself + downstream)
2
Reference proof premises (reachable / held-out)
1 / 1

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

No configuration has attempted this theorem yet.

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

instance smulCommClass₀' [SMul α G₀] [SMulCommClass G₀ α G₀] [IsScalarTower α G₀ G₀] :
    SMulCommClass (ConjAct G₀) α G₀ :=
  haveI := SMulCommClass.symm G₀ α G₀
  .symm ..