scope of `ring`

Stream: mathlib4

[Matthew Ballard]

From the doc string of the basic module for ring,

# `ring` tactic

A tactic for solving equations in commutative (semi)rings,
where the exponents can also contain variables.
Based on <http://www.cs.ru.nl/~freek/courses/tt-2014/read/10.1.1.61.3041.pdf> .

More precisely, expressions of the following form are supported:
- constants (non-negative integers)
- variables
- coefficients (any rational number, embedded into the (semi)ring)
- addition of expressions
- multiplication of expressions (`a * b`)
- scalar multiplication of expressions (`n • a`; the multiplier must have type `ℕ`)
- exponentiation of expressions (the exponent must have type `ℕ`)
- subtraction and negation of expressions (if the base is a full ring)

Given this why are div and inv in scope?

[Ruben Van de Velde]

Are they?

[Matthew Ballard]

I guess just for Rat for the scope

[Matthew Ballard]

Ruben Van de Velde said:

Are they?

Eg, see docs#Mathlib.Tactic.evalDiv

[Matthew Ballard]

Docstring

/-- Divides two polynomials `va, vb` to get a normalized result polynomial.

* `a / b = a * b⁻¹`
-/

[Mario Carneiro]

These functions do what they can with division, but the normal form is still polynomials so it's not that much. Having basic support means for example that they can prove a / b = a * b⁻¹, which is important in particular if a is a sum, since then you still have some polynomial structure to extract

[Matthew Ballard]

But should they or should it be in some type of extension? I mention this because it imports a good deal of machinery compared to what is used.

[Mario Carneiro]

I said this already when the same question was raised about abel: I think we should separate the definition of fundamental algebraic structures from the more high powered results that use these tactics. I see no reason we can't blitz our way to Field, instantiate these tactics, and then redo group theory etc with more completeness. In other words: there should be a Algebra.Field.Defs and ring and abel should not be used in the dependencies of that file

[Yaël Dillies]

I have plans along those lines, starting with order theory (because it is shorter and because I am roughly the only one caring about it). Keep your eyes peeled.

[Kim Morrison]

Mario Carneiro said:

In other words: there should be a Algebra.Field.Defs and ring and abel should not be used in the dependencies of that file

This has been the case for a while?

[Matthew Ballard]

Yes, now I am confused too.

More directly: does it make sense to split up ring so that the core part avoids division and inversion?