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