[Merged by Bors] - feat: show that `BitVec` is a commutative ring#8711

Closed

alexkeizer wants to merge 28 commits intomasterfrom bitvec-ring

+120-1

Commits on Dec 8, 2023

feat: show that BitVec is a commutative ring

alexkeizer
authored and
tobiasgrosser
committed
add toFin_injective

alexkeizer
authored and
tobiasgrosser
committed
reverse direction of ofFin_foo_ofFin

alexkeizer
authored and
tobiasgrosser
committed
WIP

alexkeizer
authored and
tobiasgrosser
committed
rename lemma to reflect to changed order

alexkeizer
authored and
tobiasgrosser
committed
reorder Injectivivity proofs

alexkeizer
authored and
tobiasgrosser
committed
refactor distributivity lemmas

alexkeizer
authored and
tobiasgrosser
committed
remove extraneous arguments

alexkeizer
authored and
tobiasgrosser
committed
add ofFin_zero/_one

alexkeizer
authored and
tobiasgrosser
committed
add toFin_zero/_one

alexkeizer
authored and
tobiasgrosser
committed
refactor SMul, Pow and Cast instances

alexkeizer
authored and
tobiasgrosser
committed
move instances to Defs file, use theorems by name

alexkeizer
authored and
tobiasgrosser
committed
Remove some simp lemmas
tobiasgrosser
committed
Update Mathlib/Data/Bitvec/Lemmas.lean

tobiasgrosser
and
eric-wieser
committed
tidy

eric-wieser
authored and
tobiasgrosser
committed
Fix proofs

alexkeizer
authored and
tobiasgrosser
committed
Fix more proofs

alexkeizer
authored and
tobiasgrosser
committed
WIP: use ofInt as IntCast instance

alexkeizer
authored and
tobiasgrosser
committed
finish ofFin_intCast proof

alexkeizer
authored and
tobiasgrosser
committed

Commits on Dec 11, 2023