RingNF

📁 Source: Mathlib/Tactic/Ring/RingNF.lean

Statistics

Metric	Count
Definitions `isAtom`, `isAtom`, `isAtom`, `Config`, `failIfUnchanged`, `mode`, `toConfig`, `RingMode`, `cleanup`, `convRing!`, `convRing_nf!_`, `elabConfig`, `elabRingNFConv`, `evalExpr`, `instBEqConfig`, `beq`, `instBEqRingMode`, `beq`, `instInhabitedConfig`, `default`, `instInhabitedRingMode`, `default`, `instReprConfig`, `repr`, `instReprRingMode`, `repr`, `ring1NF`, `ringConv`, `ringNF`, `ringNFConv`, `tacticRing!`, `tacticRing1_nf!_`, `tacticRing_nf!__`	33
Theorems `add_assoc_rev`, `add_neg`, `int_rawCast_neg`, `mul_assoc_rev`, `mul_neg`, `nat_rawCast_0`, `nat_rawCast_1`, `nat_rawCast_2`, `nnrat_rawCast`, `rat_rawCast_neg`	10
Total	43

Mathlib.Tactic.Ring.ExBase

Definitions

Name	Category	Theorems
`isAtom` 📖	CompOp	—

Mathlib.Tactic.Ring.ExProd

Definitions

Name	Category	Theorems
`isAtom` 📖	CompOp	—

Mathlib.Tactic.Ring.ExSum

Definitions

Name	Category	Theorems
`isAtom` 📖	CompOp	—

Mathlib.Tactic.RingNF

Definitions

Name	Category	Theorems
`Config` 📖	CompData	—
`RingMode` 📖	CompData	—
`cleanup` 📖	CompOp	—
`convRing!` 📖	CompOp	—
`convRing_nf!_` 📖	CompOp	—
`elabConfig` 📖	CompOp	—
`elabRingNFConv` 📖	CompOp	—
`evalExpr` 📖	CompOp	—
`instBEqConfig` 📖	CompOp	—
`instBEqRingMode` 📖	CompOp	—
`instInhabitedConfig` 📖	CompOp	—
`instInhabitedRingMode` 📖	CompOp	—
`instReprConfig` 📖	CompOp	—
`instReprRingMode` 📖	CompOp	—
`ring1NF` 📖	CompOp	—
`ringConv` 📖	CompOp	—
`ringNF` 📖	CompOp	—
`ringNFConv` 📖	CompOp	—
`tacticRing!` 📖	CompOp	—
`tacticRing1_nf!_` 📖	CompOp	—
`tacticRing_nf!__` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_assoc_rev` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`add_assoc`
`add_neg` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`sub_eq_add_neg`
`int_rawCast_neg` 📖	mathematical	—	`Int.rawCast` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Nat.rawCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Int.cast_negOfNat`
`mul_assoc_rev` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`mul_assoc`
`mul_neg` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`mul_neg`
`nat_rawCast_0` 📖	mathematical	—	`Nat.rawCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Nat.cast_zero`
`nat_rawCast_1` 📖	mathematical	—	`Nat.rawCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne`	—	`Nat.cast_one`
`nat_rawCast_2` 📖	mathematical	—	`Nat.rawCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast`	—	—
`nnrat_rawCast` 📖	mathematical	—	`NNRat.rawCast` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Nat.rawCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring`	—	—
`rat_rawCast_neg` 📖	mathematical	—	`Rat.rawCast` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Int.rawCast` `DivisionRing.toRing` `Nat.rawCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Int.cast_negOfNat`

Mathlib.Tactic.RingNF.Config

Definitions

Name	Category	Theorems
`failIfUnchanged` 📖	CompOp	—
`mode` 📖	CompOp	—
`toConfig` 📖	CompOp	—

Mathlib.Tactic.RingNF.instBEqConfig

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Mathlib.Tactic.RingNF.instBEqRingMode

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Mathlib.Tactic.RingNF.instInhabitedConfig

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Tactic.RingNF.instInhabitedRingMode

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Tactic.RingNF.instReprConfig

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

Mathlib.Tactic.RingNF.instReprRingMode

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

---

← Back to Index