R : Type ?u.773122
M : Type ?u.773125
inst✝²² : Semiring R
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
R₁ : Type ?u.773161
M₁ : Type ?u.773164
inst✝¹⁹ : Ring R₁
inst✝¹⁸ : AddCommGroup M₁
inst✝¹⁷ : Module R₁ M₁
R₂ : Type ?u.773773
M₂ : Type ?u.773776
inst✝¹⁶ : CommSemiring R₂
inst✝¹⁵ : AddCommMonoid M₂
inst✝¹⁴ : Module R₂ M₂
R₃ : Type ?u.773963
M₃ : Type ?u.773966
inst✝¹³ : CommRing R₃
inst✝¹² : AddCommGroup M₃
inst✝¹¹ : Module R₃ M₃
V : Type ?u.774554
K : Type ?u.774557
inst✝¹⁰ : Field K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.775771
M₂'' : Type ?u.775774
inst✝⁷ : AddCommMonoid M₂'
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : Module R₂ M₂'
inst✝⁴ : Module R₂ M₂''
R₄ : Type u_1
M₄ : Type u_2
inst✝³ : Ring R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ bilin G (a • x) y = 0 ↔ bilin G x y = 0
R : Type ?u.773122
M : Type ?u.773125
inst✝²² : Semiring R
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
R₁ : Type ?u.773161
M₁ : Type ?u.773164
inst✝¹⁹ : Ring R₁
inst✝¹⁸ : AddCommGroup M₁
inst✝¹⁷ : Module R₁ M₁
R₂ : Type ?u.773773
M₂ : Type ?u.773776
inst✝¹⁶ : CommSemiring R₂
inst✝¹⁵ : AddCommMonoid M₂
inst✝¹⁴ : Module R₂ M₂
R₃ : Type ?u.773963
M₃ : Type ?u.773966
inst✝¹³ : CommRing R₃
inst✝¹² : AddCommGroup M₃
inst✝¹¹ : Module R₃ M₃
V : Type ?u.774554
K : Type ?u.774557
inst✝¹⁰ : Field K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.775771
M₂'' : Type ?u.775774
inst✝⁷ : AddCommMonoid M₂'
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : Module R₂ M₂'
inst✝⁴ : Module R₂ M₂''
R₄ : Type u_1
M₄ : Type u_2
inst✝³ : Ring R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ IsOrtho G (a • x) y ↔ IsOrtho G x y
dsimp only [IsOrtho]
no goals
R : Type ?u.773122
M : Type ?u.773125
inst✝²² : Semiring R
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
R₁ : Type ?u.773161
M₁ : Type ?u.773164
inst✝¹⁹ : Ring R₁
inst✝¹⁸ : AddCommGroup M₁
inst✝¹⁷ : Module R₁ M₁
R₂ : Type ?u.773773
M₂ : Type ?u.773776
inst✝¹⁶ : CommSemiring R₂
inst✝¹⁵ : AddCommMonoid M₂
inst✝¹⁴ : Module R₂ M₂
R₃ : Type ?u.773963
M₃ : Type ?u.773966
inst✝¹³ : CommRing R₃
inst✝¹² : AddCommGroup M₃
inst✝¹¹ : Module R₃ M₃
V : Type ?u.774554
K : Type ?u.774557
inst✝¹⁰ : Field K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.775771
M₂'' : Type ?u.775774
inst✝⁷ : AddCommMonoid M₂'
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : Module R₂ M₂'
inst✝⁴ : Module R₂ M₂''
R₄ : Type u_1
M₄ : Type u_2
inst✝³ : Ring R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ bilin G (a • x) y = 0 ↔ bilin G x y = 0
rw [smul_left, mul_eq_zero, or_iff_right ha]