Type vars in `data/polynomial/splitting_field`

[urkud]

Some parts of the file use [field R]. This looks strange to me.

[bryangingechen]

We don't have a data/polynomial/splitting_field.lean (anymore?). Is the issue about code in field_theory/splitting_field.lean?

[jcommelin]

Here's the list of all places where we currently assume [field R].

$ rg "\\[field R\\]"
src/algebra/field.lean
198:lemma field.to_is_field (R : Type u) [field R] : is_field R :=

src/linear_algebra/matrix.lean
653:variables {R : Type v} [field R]

src/ring_theory/algebra_tower.lean
193:variables [field R] [division_ring S] [algebra R S] [char_zero R] [char_zero S]

src/algebra/algebra/subalgebra.lean
393:theorem bijective_algebra_map_iff {R A : Type*} [field R] [semiring A] [nontrivial A] [algebra R A] :

src/algebra/module/basic.lean
263:abbreviation vector_space (R : Type u) (M : Type v) [field R] [add_comm_group M] :=

src/algebra/module/submodule.lean
207:  [field R] [add_comm_group M] [vector_space R M] :=

src/data/polynomial/field_division.lean
54:variables [field R] {p q : polynomial R}

src/topology/algebra/module.lean
86:  [field R] [topological_space R]
141:[field R] [topological_space R]