Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-04 23:27 7aaccae7

View on Github →

feat(algebra/char_p,field_theory/finite_card): cardinality of finite fields (#819)

  • First lemma's added
  • fixed lemmas by switching arguments
  • vector_space card_fin
  • char p implies zmod p module
  • Finite field card
  • renaming
  • .
  • bug fix
  • move to_module to is_ring_hom.to_module
  • fix bug
  • remove unnecessary open
  • instance instead of thm and remove unnecessary variables
  • moved cast_is_ring_hom and zmod.to_module to char_p
  • removed redundent nat.prime
  • some char_p stuff inside namespace char_p
  • fix
  • Moved finite field card to a different file
  • Removed unnecessary import
  • Remove unnecessary lemmas
  • Update src/algebra/char_p.lean Co-Authored-By: CPutz casper.putz@gmail.com
  • rename char_p lemmas
  • Minor changes

Estimated changes