English
For any R with NatCast, and n ≥ 2, there exists an OfNat R n given by ofNat := n.cast.
Русский
Для любого R с NatCast и n ≥ 2 существует OfNat R n, заданный as ofNat := n.cast.
LaTeX
$$$$ \text{OfNat } R\, n \text{ where } n \ge 2 \text{ is given by } \text{ofNat} := n.cast $$$$
Lean4
/-- Recognize numeric literals which are at least `2` as terms of `R` via `Nat.cast`. This
instance is what makes things like `37 : R` type check. Note that `0` and `1` are not needed
because they are recognized as terms of `R` (at least when `R` is an `AddMonoidWithOne`) through
`Zero` and `One`, respectively. -/
@[nolint unusedArguments]
instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : OfNat R n where ofNat := n.cast
