Revision #1567 → #2671 · back to history
c707502d0faf| Field | From #1567 | To #2671 |
|---|---|---|
| mathlib.decl | Basis.addHaar_parallelepiped | MeasureTheory.Measure.addHaar_parallelepiped |
| provenance | ai | ai-moderated |
8fae9c7d336e| Field | From #1567 | To #2671 |
|---|---|---|
| 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 |