Mathlib v3 is deprecated. Go to Mathlib v4

Theorem coe_bit0

Modification history

2022-11-28 20:07

src/algebra/hom/group.lean

chore(*): revert #17048 (#17733) …

Deleted coe_bit0 View on Github →

2022-11-09 17:39

src/algebra/hom/group.lean

feat(*): define classes for coercions that are homomorphisms (#17048) …

Added coe_bit0 View on Github →

2020-04-16 08:33

test/norm_cast_cardinal.lean

refactor(tactic/norm_cast): simplified attributes and numeral support (#2407) …

Added coe_bit0 View on Github →