feat: extend LawfulXor lemmas and add Equiv.xor

[linesthatinterlace]

This PR extends the work of #37712 by adding additional lemmas and adding xor-as-a-permutation.

---

[github-actions]

PR summary 10b21fc2a1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Fin.Init (new file)	55
Mathlib.Data.LawfulXor.Basic (new file)	86
Mathlib.Data.LawfulXor.Equiv (new file)	348

---

Declarations diff

+ LawfulXor
+ instance : LawfulXor ISize
+ instance : LawfulXor Int16
+ instance : LawfulXor Int32
+ instance : LawfulXor Int64
+ instance : LawfulXor Int8
+ instance : LawfulXor Nat
+ instance : LawfulXor UInt16
+ instance : LawfulXor UInt32
+ instance : LawfulXor UInt64
+ instance : LawfulXor UInt8
+ instance : LawfulXor USize
+ instance : Std.Associative (α := α) XorOp.xor where assoc := xor_assoc
+ instance : Std.Commutative (α := α) XorOp.xor where comm := xor_comm
+ instance : Std.LawfulCommIdentity (α := α) XorOp.xor 0
+ instance {w : Nat} : LawfulXor (BitVec w)
+ instance {w : ℕ} : LawfulXor (Fin (2 ^ w))
+ isFixedPt_xor
+ isFixedPt_xor_left_iff
+ isFixedPt_xor_right_iff
+ not_isFixedPt_xor_left_of_neZero
+ not_isFixedPt_xor_of_neZero
+ not_isFixedPt_xor_right_of_neZero
+ xor
+ xor_apply_comm
+ xor_apply_eq_zero_iff
+ xor_apply_xor_apply
+ xor_assoc
+ xor_cancel_left
+ xor_cancel_right
+ xor_comm
+ xor_eq_iff_left_eq
+ xor_eq_iff_right_eq
+ xor_eq_one_iff
+ xor_eq_zero_iff
+ xor_involutive
+ xor_left_eq_self
+ xor_left_id_iff
+ xor_left_involutive
+ xor_left_zero
+ xor_right_eq_self
+ xor_right_id_iff
+ xor_right_involutive
+ xor_right_zero
+ xor_self
+ xor_self_apply
+ xor_symm
+ xor_trans_xor
+ xor_xor_cancel_comm
+ xor_xor_cancel_comm_assoc
+ xor_zero_apply
+ zero_xor
++ xor_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[linesthatinterlace]

As a note: I think one can sensibly consider the notion of "xor-respecting maps", BUT right now I don't see any need for this.

[linesthatinterlace]

(In contrast the fixed-point lemmas and the equivalence I add here do come up in practice and are IMO a characteristic property of a Lawful Xor).