Revision #1918 → #2674 · back to history
4e74a1b27231| Field | From #1918 | To #2674 |
|---|---|---|
| mathlib.decl | norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two | InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two |
| provenance | ai | ai-moderated |