Zulip Chat Archive

Stream: general

Topic: cardinality of a field

Eric Rodriguez (Feb 18 2022 at 16:01):

I've now finished the result in full generality! (I'm moving this away from the thread that I hijacked, sorry Jireh)

Field is p^k or any possible cardinality

this needs cleaning up, but I have to run - I'm happy for anyone to fix things up! I left a couple comments about my frustrations...

cc: @Mario Carneiro @Alex J. Best who seemed interested

Alex J. Best (Feb 18 2022 at 16:18):

Nice, the last 3 lines can just be simpa I think

Alex J. Best (Feb 18 2022 at 16:20):

And docs#finsupp.single_eq_single_iff exists so you can do

lemma monomial_ext_iff {α} {R} [comm_semiring R] {a b : α →₀ } {c d : R} (hc : c  0) :
  mv_polynomial.monomial a c = mv_polynomial.monomial b d  a = b  c = d :=
  convert finsupp.single_eq_single_iff _ _ _ _,
  simp [hc],

Eric Rodriguez (Feb 18 2022 at 16:51):

Also, i just realised the general result can just be is_prime_power #a - as all infinite cardinals are prime :) (probably too cute though)

Kevin Buzzard (Feb 18 2022 at 18:26):

wait, if κ\kappa is an infinite cardinal then κ=κ×κ\kappa=\kappa\times\kappa right?

Eric Rodriguez (Feb 25 2022 at 11:14):

the result (modulo cute cardinal stuff) is finally pr'd! #12285 (I need #12197 for the cute cardinal stuff)

Eric Rodriguez (Mar 04 2022 at 00:36):

(and we have cute cardinal stuff on #12442)

Last updated: Aug 03 2023 at 10:10 UTC