Theorems · Theorem · general algebraic systems

FunLike.intCast_eq_zsmul_one

∀ {F' : Type u_4} {α : Type u_5} [inst : FunLike F' α α] [inst_1 : IntCast F'] [inst_2 : One F'] [inst_3 : SMul ℤ α]
  [inst_4 : SMul ℤ F'] [IsSMulApply ℤ F' α α] [IsIntCastApply F' α] [IsOneApplyEqSelf F' α] (n : ℤ), ↑n = n • 1

Defined in

Mathlib.Data.FunLike.IsApply

Cited by

1 results in Mathlib

Foundations

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

Assumes

FunLikeIntCastOneSMulSMulIsSMulApplyIsIntCastApplyIsOneApplyEqSelf