Commit 2025-02-08 10:17 5b94d7fd

View on Github →

chore(Geometry): use numeric subscripts for indices (#21548)

Estimated changes

Modified Archive/Wiedijk100Theorems/HeronsFormula.lean

modified theorem Theorems100.heron

Modified Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean

modified theorem EuclideanGeometry.angle_eq_angle_of_angle_eq_pi

modified theorem EuclideanGeometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi

modified theorem EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_left

modified theorem EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_right

modified theorem EuclideanGeometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq

modified theorem EuclideanGeometry.angle_midpoint_eq_pi

modified theorem EuclideanGeometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq

modified theorem EuclideanGeometry.dist_eq_abs_sub_dist_iff_angle_eq_zero

modified theorem EuclideanGeometry.dist_eq_abs_sub_dist_of_angle_eq_zero

modified theorem EuclideanGeometry.dist_eq_add_dist_iff_angle_eq_pi

modified theorem EuclideanGeometry.dist_eq_add_dist_of_angle_eq_pi

modified theorem EuclideanGeometry.left_dist_ne_zero_of_angle_eq_pi

modified theorem EuclideanGeometry.right_dist_ne_zero_of_angle_eq_pi

Modified Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean

modified theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two

Modified Mathlib/Geometry/Euclidean/Basic.lean

modified theorem EuclideanGeometry.dist_left_midpoint_eq_dist_right_midpoint

modified theorem EuclideanGeometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd

Modified Mathlib/Geometry/Euclidean/Circumcenter.lean

Modified Mathlib/Geometry/Euclidean/Triangle.lean

modified theorem EuclideanGeometry.angle_add_angle_add_angle_eq_pi

modified theorem EuclideanGeometry.angle_eq_angle_of_dist_eq

modified theorem EuclideanGeometry.dist_eq_of_angle_eq_angle_of_angle_ne_pi

modified theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean

modified theorem AffineSubspace.direction_affineSpan_insert

modified theorem AffineSubspace.direction_inf

modified theorem AffineSubspace.direction_le

modified theorem AffineSubspace.direction_lt_of_nonempty

modified theorem AffineSubspace.direction_sup

modified theorem AffineSubspace.exists_of_lt

modified theorem AffineSubspace.ext_of_direction_eq

modified theorem AffineSubspace.inf_coe

modified theorem AffineSubspace.inter_eq_singleton_of_nonempty_of_isCompl

modified theorem AffineSubspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top

modified theorem AffineSubspace.le_def'

modified theorem AffineSubspace.le_def

modified theorem AffineSubspace.lt_def

modified theorem AffineSubspace.lt_iff_le_and_exists

modified theorem AffineSubspace.mem_affineSpan_insert_iff

modified theorem AffineSubspace.mem_inf_iff

modified theorem AffineSubspace.not_le_iff_exists

modified theorem AffineSubspace.spanPoints_subset_coe_of_subset_coe

modified theorem AffineSubspace.sup_direction_le

modified theorem AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty

modified theorem AffineSubspace.vsub_left_mem_direction_iff_mem

modified theorem AffineSubspace.vsub_mem_direction

modified theorem AffineSubspace.vsub_right_mem_direction_iff_mem

modified theorem vsub_mem_vectorSpan

modified theorem vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints