Commit 2023-04-25 11:42 2b42dc7c

View on Github →

chore: fix #align lines (#3640) This PR fixes two things:

  • Most align statements for definitions and theorems and instances that are separated by two newlines from the relevant declaration (s/\n\n#align/\n#align). This is often seen in the mathport output after ending calc blocks.
  • All remaining more-than-one-line #align statements. (This was needed for a script I wrote for #3630.)

Estimated changes

modified def unitary
modified theorem Nat.fast_fib_aux_eq
modified theorem Nat.fib_add
modified theorem Nat.fib_add_two_strictMono
modified theorem Nat.fib_coprime_fib_succ
modified theorem Nat.fib_lt_fib_succ
modified theorem Nat.fib_succ_eq_succ_sum
modified theorem Nat.fib_two_mul
modified theorem Nat.fib_two_mul_add_one
modified theorem Nat.le_fib_self