R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
⊢ BilinForm.compLeft (↑toBilin' J₃) (↑toLin' A) = BilinForm.compRight (↑toBilin' J) (↑toLin' A') ↔
    IsAdjointPair J J₃ A A'
R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
⊢ BilinForm.IsAdjointPair (↑toBilin' J) (↑toBilin' J₃) (↑toLin' A) (↑toLin' A') ↔ IsAdjointPair J J₃ A A'
rw [BilinForm.isAdjointPair_iff_compLeft_eq_compRight]
R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
h : ∀ (B B' : BilinForm R₃ (n → R₃)), B = B' ↔ ↑BilinForm.toMatrix' B = ↑BilinForm.toMatrix' B'
⊢ Aᵀ ⬝ J₃ = J ⬝ A' ↔ IsAdjointPair J J₃ A A'
R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
h : ∀ (B B' : BilinForm R₃ (n → R₃)), B = B' ↔ ↑BilinForm.toMatrix' B = ↑BilinForm.toMatrix' B'
⊢ BilinForm.compLeft (↑toBilin' J₃) (↑toLin' A) = BilinForm.compRight (↑toBilin' J) (↑toLin' A') ↔
    IsAdjointPair J J₃ A A'
rw [h, BilinForm.toMatrix'_compLeft, BilinForm.toMatrix'_compRight, LinearMap.toMatrix'_toLin',
  LinearMap.toMatrix'_toLin', BilinForm.toMatrix'_toBilin', BilinForm.toMatrix'_toBilin']
no goals
R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
h : ∀ (B B' : BilinForm R₃ (n → R₃)), B = B' ↔ ↑BilinForm.toMatrix' B = ↑BilinForm.toMatrix' B'
⊢ Aᵀ ⬝ J₃ = J ⬝ A' ↔ IsAdjointPair J J₃ A A'
rfl
R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
B B' : BilinForm R₃ (n → R₃)
⊢ B = B' ↔ ↑BilinForm.toMatrix' B = ↑BilinForm.toMatrix' B'
R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
⊢ ∀ (B B' : BilinForm R₃ (n → R₃)), B = B' ↔ ↑BilinForm.toMatrix' B = ↑BilinForm.toMatrix' B'
intro B B'
case mp
R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
B B' : BilinForm R₃ (n → R₃)
h : B = B'
⊢ ↑BilinForm.toMatrix' B = ↑BilinForm.toMatrix' B'

case mpr
R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
B B' : BilinForm R₃ (n → R₃)
h : ↑BilinForm.toMatrix' B = ↑BilinForm.toMatrix' B'
⊢ B = B'
R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
B B' : BilinForm R₃ (n → R₃)
⊢ B = B' ↔ ↑BilinForm.toMatrix' B = ↑BilinForm.toMatrix' B'
constructor <;> intro h
no goals
case mp
R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
B B' : BilinForm R₃ (n → R₃)
h : B = B'
⊢ ↑BilinForm.toMatrix' B = ↑BilinForm.toMatrix' B'
rw [h]
no goals
case mpr
R : Type ?u.1916305
M : Type ?u.1916308
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1916344
M₁ : Type ?u.1916347
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.1916956
M₂ : Type ?u.1916959
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.1917149
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1917737
K : Type ?u.1917740
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
B B' : BilinForm R₃ (n → R₃)
h : ↑BilinForm.toMatrix' B = ↑BilinForm.toMatrix' B'
⊢ B = B'
exact BilinForm.toMatrix'.injective h