Theorem coe_int_mem

Modification history

2024-04-07 17:47

Mathlib/RingTheory/Subring/Basic.lean

chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` (#11499) …

Deleted coe_int_mem View on Github →

2023-02-11 16:08

Mathlib/RingTheory/Subring/Basic.lean

feat: port RingTheory.Subring.Basic (#1945)

Added coe_int_mem View on Github →