ofEq

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

URI: https://scilib.ai/kg/mathlib#AffineEquiv.ofEq

Lean4

/-- Affine equivalence between two equal affine subspace.

This is the affine version of `LinearEquiv.ofEq`. -/
@[simps linear]
def ofEq (h : S₁ = S₂) : S₁ ≃ᵃ[k] S₂
    where
  toEquiv := Equiv.setCongr <| congr_arg _ h
  linear := .ofEq _ _ <| congr_arg _ h
  map_vadd' := fun ⟨_, _⟩ ⟨_, _⟩ => rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru