ericrbg

/-
Copyright (c) 2021 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa
-/
import data.zmod.basic
import ring_theory.subsemiring.basic
import algebra.order.monoid
/-!

ericrbg

WARNING types not equal
<def homology_zero_zero : Π {V : Type u} [_inst_1 : category_theory.category V]
[_inst_2 : category_theory.limits.has_zero_morphisms V] {A B C : V} [_inst_6 : category_theory.limits.has_zero_object V]
[_inst_7 : category_theory.limits.has_image 0]
[_inst_8 : category_theory.limits.has_cokernel (image_to_kernel 0 0 homology_zero_zero._proof_3)],
  homology 0 0 homology_zero_zero._proof_5 ≅ B := λ {V : Type u} [_inst_1 : category_theory.category V]
[_inst_2 : category_theory.limits.has_zero_morphisms V] {A B C : V} [_inst_6 : category_theory.limits.has_zero_object V]
[_inst_7 : category_theory.limits.has_image 0]
[_inst_8 : category_theory.limits.has_cokernel (image_to_kernel 0 0 homology_zero_zero._proof_8)],
  {hom := homology.desc 0 0 homology_zero_zero._proof_12 (category_theory.limits.kernel_subobject 0).arrow

ericrbg

import field_theory.finite.galois_field
import algebra.is_prime_pow
import data.equiv.transfer_instance
import data.mv_polynomial.cardinal
import data.rat.denumerable
import algebra.ring.ulift

local notation `‖` x `‖` := fintype.card x
open_locale cardinal non_zero_divisors