ENatToNat

📁 Source: Mathlib/Tactic/ENatToNat.lean

Statistics

Metric	Count
Definitions tacticCases_first_enat, tacticEnat_to_nat	2
Theorems coe_add, coe_mul, coe_ofNat, coe_one, coe_sub, coe_zero, not_lt_top	7
Total	9

Mathlib.Tactic.ENatToNat

Definitions

Name	Category	Theorems
tacticCases_first_enat 📖	CompOp	—
tacticEnat_to_nat 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_add 📖	mathematical	—	ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast	—	—
coe_mul 📖	mathematical	—	ENat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast	—	—
coe_ofNat 📖	mathematical	—	ENat instOfNatAtLeastTwo ENat.instNatCast	—	—
coe_one 📖	mathematical	—	ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast	—	—
coe_sub 📖	mathematical	—	ENat instSubENat ENat.instNatCast	—	—
coe_zero 📖	mathematical	—	ENat instZeroENat ENat.instNatCast	—	—
not_lt_top 📖	mathematical	—	ENat Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Top.top instTopENat	—	—

---

← Back to Index