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 :=
begin
convert finsupp.single_eq_single_iff _ _ _ _,
simp [hc],
end


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: Dec 20 2023 at 11:08 UTC