Theorem Linarith.natCast_nonneg

Modification history

2025-06-19 05:18

Mathlib/Tactic/Linarith/Lemmas.lean

chore(Tactic/Linarith): put linarith declarations into `Mathlib.Tactic` namespace (#25955) …

Deleted Linarith.natCast_nonneg View on Github →

2025-04-09 10:22

Mathlib/Tactic/Linarith/Lemmas.lean

chore: use mixin ordered algebraic typeclasses (part 2) (#20595)

Modified Linarith.natCast_nonneg View on Github →

2024-04-17 11:15

Mathlib/Tactic/Linarith/Lemmas.lean

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

Added Linarith.natCast_nonneg View on Github →