Commit 2023-12-15 16:32 1250aa83

View on Github →

feat: show that BitVec is a commutative ring (#8711)

Estimated changes

Modified Mathlib/Data/BitVec/Defs.lean

Modified Mathlib/Data/BitVec/Lemmas.lean

added theorem Std.BitVec.ofFin_add

added theorem Std.BitVec.ofFin_and

added theorem Std.BitVec.ofFin_mul

added theorem Std.BitVec.ofFin_natCast

added theorem Std.BitVec.ofFin_neg

added theorem Std.BitVec.ofFin_nsmul

added theorem Std.BitVec.ofFin_ofNat

added theorem Std.BitVec.ofFin_one

added theorem Std.BitVec.ofFin_or

added theorem Std.BitVec.ofFin_pow

added theorem Std.BitVec.ofFin_sub

added theorem Std.BitVec.ofFin_xor

added theorem Std.BitVec.ofFin_zero

added theorem Std.BitVec.ofFin_zsmul

added theorem Std.BitVec.toFin_add

added theorem Std.BitVec.toFin_and

added theorem Std.BitVec.toFin_inj

added theorem Std.BitVec.toFin_injective

added theorem Std.BitVec.toFin_mul

added theorem Std.BitVec.toFin_natCast

added theorem Std.BitVec.toFin_neg

added theorem Std.BitVec.toFin_nsmul

added theorem Std.BitVec.toFin_ofNat

added theorem Std.BitVec.toFin_one

added theorem Std.BitVec.toFin_or

added theorem Std.BitVec.toFin_pow

added theorem Std.BitVec.toFin_sub

added theorem Std.BitVec.toFin_xor

added theorem Std.BitVec.toFin_zero

added theorem Std.BitVec.toFin_zsmul

modified theorem Std.BitVec.toNat_injective