Theorems · Definition · group theory
Equiv.pointReflection
{G : Type u_3} → {P : Type u_4} → [inst : AddGroup G] → [AddTorsor G P] → P → Equiv.Perm PPoint reflection in x as a permutation.
- Defined in
- Mathlib.Algebra.Torsor.Defs
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- AddTorsorstatement and proof · cited by 1,657
- Equiv.Permstatement · cited by 1,375
- Equiv.transproof · cited by 337
- Equiv.vaddConstproof · cited by 8
- Equiv.constVSubproof · cited by 3
Cited by35
Results whose statement or proof uses this declaration.
- Equiv.pointReflection_applystatement · cited by 5
- Equiv.pointReflection_involutivestatement and proof · cited by 4
- midpoint_pointReflection_rightstatement · cited by 3
- isImmersionOfComplement_subtypeVal_Iccproof · cited by 3
- Equiv.pointReflection_midpoint_leftstatement and proof · cited by 2
- Equiv.pointReflection_symmstatement · cited by 2
- Equiv.pointReflection_vsub_leftstatement · cited by 2
- Equiv.pointReflection_vsub_rightstatement · cited by 2
- EuclideanGeometry.Sphere.IsDiameter.pointReflection_center_leftstatement and proof · cited by 2
- EuclideanGeometry.Sphere.isDiameter_iff_left_mem_and_pointReflection_center_leftstatement and proof · cited by 1
- midpoint_eq_iff'statement · cited by 1
- midpoint_pointReflection_leftstatement · cited by 1