mathlib3

68f41d3c - chore(number_theory/ramification_inertia): make an argument explicit (#17890)

chore(number_theory/ramification_inertia): make an argument explicit (#17890) This makes it slightly easier to use the `ideal.factors.pi_quotient_linear_equiv` definition, as otherwise all the typeclass search on properties of `S` is postponed till after the proof argument `hp : map (algebra_map R S) p ≠ ⊥` is provided.