R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.6685
M : Type ?u.6688
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.6697
Mₗ₁' : Type ?u.6700
Mₗ₂ : Type ?u.6703
Mₗ₂' : Type ?u.6706
K : Type ?u.6709
K₁ : Type ?u.6712
K₂ : Type ?u.6715
V : Type ?u.6718
V₁ : Type ?u.6721
V₂ : Type ?u.6724
n : Type ?u.6727
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
x : M₂
⊢ ↑(↑B 0) x = 0
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.6685
M : Type ?u.6688
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.6697
Mₗ₁' : Type ?u.6700
Mₗ₂ : Type ?u.6703
Mₗ₂' : Type ?u.6706
K : Type ?u.6709
K₁ : Type ?u.6712
K₂ : Type ?u.6715
V : Type ?u.6718
V₁ : Type ?u.6721
V₂ : Type ?u.6724
n : Type ?u.6727
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
x : M₂
⊢ IsOrtho B 0 x
dsimp only [IsOrtho]
no goals
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.6685
M : Type ?u.6688
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.6697
Mₗ₁' : Type ?u.6700
Mₗ₂ : Type ?u.6703
Mₗ₂' : Type ?u.6706
K : Type ?u.6709
K₁ : Type ?u.6712
K₂ : Type ?u.6715
V : Type ?u.6718
V₁ : Type ?u.6721
V₂ : Type ?u.6724
n : Type ?u.6727
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
x : M₂
⊢ ↑(↑B 0) x = 0
rw [map_zero B, zero_apply]