Loogle!

Result

Found 25 declarations mentioning Orientation.map.

• Orientation.map_refl 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] (ι : Type u_4) : Orientation.map ι (LinearEquiv.refl R M) = Equiv.refl (Orientation R M ι)
• Orientation.map 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (ι : Type u_4) (e : M ≃ₗ[R] N) : Orientation R M ι ≃ Orientation R N ι
• Orientation.map_of_isEmpty 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] (ι : Type u_4) [IsEmpty ι] (x : Orientation R M ι) (f : M ≃ₗ[R] M) : (Orientation.map ι f) x = x
• Orientation.map_symm 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (ι : Type u_4) (e : M ≃ₗ[R] N) : (Orientation.map ι e).symm = Orientation.map ι e.symm
• Orientation.map_positiveOrientation_of_isEmpty 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (ι : Type u_4) [IsEmpty ι] (f : M ≃ₗ[R] N) : (Orientation.map ι f) positiveOrientation = positiveOrientation
• Basis.orientation_map 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (e : Basis ι R M) (f : M ≃ₗ[R] N) : (e.map f).orientation = (Orientation.map ι f) e.orientation
• Orientation.map.eq_1 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (ι : Type u_4) (e : M ≃ₗ[R] N) : Orientation.map ι e = Module.Ray.map (AlternatingMap.domLCongr R R ι R e)
• Orientation.map_neg 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {ι : Type u_4} (f : M ≃ₗ[R] N) (x : Orientation R M ι) : (Orientation.map ι f) (-x) = -(Orientation.map ι f) x
• Orientation.map_eq_iff_det_pos 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [FiniteDimensional R M] (x : Orientation R M ι) (f : M ≃ₗ[R] M) (h : Fintype.card ι = Module.finrank R M) : (Orientation.map ι f) x = x ↔ 0 < LinearMap.det ↑f
• Orientation.map_eq_neg_iff_det_neg 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] (x : Orientation R M ι) (f : M ≃ₗ[R] M) (h : Fintype.card ι = Module.finrank R M) : (Orientation.map ι f) x = -x ↔ LinearMap.det ↑f < 0
• Orientation.map_apply 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (ι : Type u_4) (e : M ≃ₗ[R] N) (v : M [⋀^ι]→ₗ[R] R) (hv : v ≠ 0) : (Orientation.map ι e) (rayOfNeZero R v hv) = rayOfNeZero R (v.compLinearMap ↑e.symm) ⋯
• Basis.map_orientation_eq_det_inv_smul 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] (e : Basis ι R M) (x : Orientation R M ι) (f : M ≃ₗ[R] M) : (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x
• Orientation.map_eq_det_inv_smul 📋 Mathlib.LinearAlgebra.Orientation
  {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] [FiniteDimensional R M] (x : Orientation R M ι) (f : M ≃ₗ[R] M) (h : Fintype.card ι = Module.finrank R M) : (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x
• Orientation.volumeForm_map 📋 Mathlib.Analysis.InnerProductSpace.Orientation
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fact (Module.finrank ℝ F = n)] (φ : E ≃ₗᵢ[ℝ] F) (x : Fin n → F) : ((Orientation.map (Fin n) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)
• Orientation.rightAngleRotation_map' 📋 Mathlib.Analysis.InnerProductSpace.TwoDim
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fact (Module.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) : ((Orientation.map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation = (φ.symm.trans o.rightAngleRotation).trans φ
• Orientation.rightAngleRotation_map 📋 Mathlib.Analysis.InnerProductSpace.TwoDim
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [hF : Fact (Module.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x : F) : ((Orientation.map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation x = φ (o.rightAngleRotation (φ.symm x))
• Orientation.rightAngleRotation_map_complex 📋 Mathlib.Analysis.InnerProductSpace.TwoDim
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x : E) : f (o.rightAngleRotation x) = Complex.I * f x
• Orientation.areaForm_map_complex 📋 Mathlib.Analysis.InnerProductSpace.TwoDim
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x y : E) : (o.areaForm x) y = ((starRingEnd ℂ) (f x) * f y).im
• Orientation.kahler_map_complex 📋 Mathlib.Analysis.InnerProductSpace.TwoDim
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x y : E) : (o.kahler x) y = f y * (starRingEnd ℂ) (f x)
• Orientation.areaForm_map 📋 Mathlib.Analysis.InnerProductSpace.TwoDim
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [hF : Fact (Module.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x y : F) : (((Orientation.map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = (o.areaForm (φ.symm x)) (φ.symm y)
• Orientation.kahler_map 📋 Mathlib.Analysis.InnerProductSpace.TwoDim
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [hF : Fact (Module.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x y : F) : (((Orientation.map (Fin 2) φ.toLinearEquiv) o).kahler x) y = (o.kahler (φ.symm x)) (φ.symm y)
• Orientation.oangle_map 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} {V' : Type u_2} [NormedAddCommGroup V] [NormedAddCommGroup V'] [InnerProductSpace ℝ V] [InnerProductSpace ℝ V'] [Fact (Module.finrank ℝ V = 2)] [Fact (Module.finrank ℝ V' = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V') (f : V ≃ₗᵢ[ℝ] V') : ((Orientation.map (Fin 2) f.toLinearEquiv) o).oangle x y = o.oangle (f.symm x) (f.symm y)
• Orientation.oangle_map_complex 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (f : V ≃ₗᵢ[ℝ] ℂ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x y : V) : o.oangle x y = ↑((starRingEnd ℂ) (f x) * f y).arg
• Orientation.rotation_map 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
  {V : Type u_1} {V' : Type u_2} [NormedAddCommGroup V] [NormedAddCommGroup V'] [InnerProductSpace ℝ V] [InnerProductSpace ℝ V'] [Fact (Module.finrank ℝ V = 2)] [Fact (Module.finrank ℝ V' = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (f : V ≃ₗᵢ[ℝ] V') (x : V') : (((Orientation.map (Fin 2) f.toLinearEquiv) o).rotation θ) x = f ((o.rotation θ) (f.symm x))
• Orientation.rotation_map_complex 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (f : V ≃ₗᵢ[ℝ] ℂ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x : V) : f ((o.rotation θ) x) = ↑θ.toCircle * f x

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision bce1d65