Commit 2024-03-01 17:22 0257770c
View on Github →chore: rename induction principle arguments around CliffordAlgebra
(#10908)
In order to improve the ergonomics of the induction
tactic, this renames the arguments of:
ExteriorAlgebra.induction
TensorAlgebra.induction
CliffordAlgebra.induction
CliffordAlgebra.left_induction
CliffordAlgebra.right_induction
CliffordAlgebra.even_induction
CliffordAlgebra.odd_induction
Submodule.iSup_induction'
Submodule.pow_induction_on_left'
Submodule.pow_induction_on_right'
This is slightly awkward for name-resolution within these induction principles, as the argument names end up clashing with the function they are about. Thankfully, this pain is not transferred to the caller usinginduction _ using _
.