first argument of minimal_polynomial necessary

Stream: general

[Kenny Lau]

import data.polynomial field_theory.subfield algebra.group_ring_action field_theory.minimal_polynomial

set_option profiler true

universes u v

variables (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] (g : G)

def fixed : set F :=
{ x | ∀ g : G, g • x = x }

instance fixed.is_subfield : is_subfield (fixed G F) :=
sorry

instance fixed.algebra : algebra (fixed G F) F :=
algebra.of_subring _

variables (x : F)

theorem is_integral_fixed : is_integral (fixed G F) x :=
sorry

#check @minimal_polynomial (fixed G F) _ _ _ _ _ (is_integral_fixed G F x)
#check @minimal_polynomial _ _ _ _ _ _ (is_integral_fixed G F x) -- very slow

[Kenny Lau]

currently the first argument (the base field) is implicit

[Kenny Lau]

but it seems that Lean cannot infer it

[Kenny Lau]

I suppose type ascription also solves it:

#check (minimal_polynomial (is_integral_fixed G F x) : polynomial (fixed G F)) -- not slow

[Johan Commelin]

I guess that most of the time this will not be slow, right?

[Yury G. Kudryashov]

BTW, why can't it infer fixed G F from is_integral_fixed G F x : is_integral (fixed G F) x?

[Yury G. Kudryashov]

OTOH, if A is an algebra over two different rings, then minimal_polynomial R x _ in pretty-printer output looks better than minimal_polynomial x _.

[Johan Commelin]

Yes, that's right. I think that is a good argument for making it explicit.