Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.eq_sq_add_sq_of_is_square_mod_neg_one

Modification history

2023-06-01 20:20

src/number_theory/sum_two_squares.lean

feat(number_theory/sum_two_squares): add result for general n (#19054) …

Added nat.eq_sq_add_sq_of_is_square_mod_neg_one View on Github →