Theorem Cardinal.natCast_injective

Modification history

2024-10-23 04:26

Mathlib/SetTheory/Cardinal/Basic.lean

chore(SetTheory/Cardinal/Basic): deprecate duplicate `Nat.cast` lemmas (#17850) …

Modified Cardinal.natCast_injective View on Github →

2023-02-11 10:18

Mathlib/SetTheory/Cardinal/Basic.lean

feat: port SetTheory.Cardinal.Basic (#2084)

Added Cardinal.natCast_injective View on Github →