@[class]
- cast_injective : function.injective coe
Typeclass for monoids with characteristic zero. (This is usually stated on fields but it makes sense for any additive monoid with 1.)
theorem
char_zero_of_inj_zero
{R : Type u_1}
[add_left_cancel_monoid R]
[has_one R]
(H : ∀ (n : ℕ), ↑n = 0 → n = 0) :
@[instance]
@[simp]
@[instance]
@[simp]
@[simp]
@[instance]