Stream: general

Topic: first argument of minimal_polynomial necessary

Kenny Lau (May 02 2020 at 07:17):

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 (May 02 2020 at 07:17):

currently the first argument (the base field) is implicit

Kenny Lau (May 02 2020 at 07:17):

but it seems that Lean cannot infer it

Kenny Lau (May 02 2020 at 07:18):

I suppose type ascription also solves it:

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


Johan Commelin (May 02 2020 at 07:48):

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

Yury G. Kudryashov (May 02 2020 at 08:24):

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 (May 02 2020 at 08:27):

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 (May 02 2020 at 08:32):

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

Last updated: May 15 2021 at 23:13 UTC