Theorem AddMonoidHom.eq_int_castAddHom

Modification history

2024-04-17 11:15

Mathlib/Data/Int/Cast/Lemmas.lean

chore: Rename `nat_cast`/`int_cast`/`rat_cast` to `natCast`/`intCast`/`ratCast` (#11486) …

Deleted AddMonoidHom.eq_int_castAddHom View on Github →

2023-01-06 13:41

Mathlib/Data/Int/Cast/Lemmas.lean

chore: rename some 'int_cast' to 'intCast' (#1337)

Added AddMonoidHom.eq_int_castAddHom View on Github →