Skip to content

[Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Basic): Delete infered instances #12122

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - refactor(LinearAlgebra/BilinearForm/Basic): Delete infered instances #12122

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 0 additions & 39 deletions Mathlib/LinearAlgebra/BilinearForm/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,8 +136,6 @@ theorem ext_iff : B = D ↔ ∀ x y, B x y = D x y :=
⟨congr_fun, ext₂⟩
#align bilin_form.ext_iff LinearMap.BilinForm.ext_iff

instance : Zero (BilinForm R M) := inferInstance

theorem coe_zero : ⇑(0 : BilinForm R M) = 0 :=
rfl
#align bilin_form.coe_zero LinearMap.BilinForm.coe_zero
Expand All @@ -149,8 +147,6 @@ theorem zero_apply (x y : M) : (0 : BilinForm R M) x y = 0 :=

variable (B D B₁ D₁)

instance : Add (BilinForm R M) := inferInstance

theorem coe_add : ⇑(B + D) = B + D :=
rfl
#align bilin_form.coe_add LinearMap.BilinForm.coe_add
Expand All @@ -160,32 +156,9 @@ theorem add_apply (x y : M) : (B + D) x y = B x y + D x y :=
rfl
#align bilin_form.add_apply LinearMap.BilinForm.add_apply

/-- `BilinForm R M` inherits the scalar action by `α` on `R` if this is compatible with
multiplication.

When `R` itself is commutative, this provides an `R`-action via `Algebra.id`. -/
instance {α} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] : SMul α (BilinForm R M) :=
inferInstance

#noalign bilin_form.coe_smul
#noalign bilin_form.smul_apply

instance {α β} [Monoid α] [Monoid β] [DistribMulAction α R] [DistribMulAction β R]
[SMulCommClass R α R] [SMulCommClass R β R] [SMulCommClass α β R] :
SMulCommClass α β (BilinForm R M) := inferInstance

instance {α β} [Monoid α] [Monoid β] [SMul α β] [DistribMulAction α R] [DistribMulAction β R]
[SMulCommClass R α R] [SMulCommClass R β R] [IsScalarTower α β R] :
IsScalarTower α β (BilinForm R M) := inferInstance

instance {α} [Monoid α] [DistribMulAction α R] [DistribMulAction αᵐᵒᵖ R]
[SMulCommClass R α R] [IsCentralScalar α R] :
IsCentralScalar α (BilinForm R M) := inferInstance

instance : AddCommMonoid (BilinForm R M) := inferInstance

instance : Neg (BilinForm R₁ M₁) := inferInstance

theorem coe_neg : ⇑(-B₁) = -B₁ :=
rfl
#align bilin_form.coe_neg LinearMap.BilinForm.coe_neg
Expand All @@ -195,8 +168,6 @@ theorem neg_apply (x y : M₁) : (-B₁) x y = -B₁ x y :=
rfl
#align bilin_form.neg_apply LinearMap.BilinForm.neg_apply

instance : Sub (BilinForm R₁ M₁) := inferInstance

theorem coe_sub : ⇑(B₁ - D₁) = B₁ - D₁ :=
rfl
#align bilin_form.coe_sub LinearMap.BilinForm.coe_sub
Expand All @@ -206,23 +177,13 @@ theorem sub_apply (x y : M₁) : (B₁ - D₁) x y = B₁ x y - D₁ x y :=
rfl
#align bilin_form.sub_apply LinearMap.BilinForm.sub_apply

instance : AddCommGroup (BilinForm R₁ M₁) := inferInstance

instance : Inhabited (BilinForm R M) := inferInstance

/-- `coeFn` as an `AddMonoidHom` -/
def coeFnAddMonoidHom : BilinForm R M →+ M → M → R where
toFun := (fun B x y => B x y)
map_zero' := rfl
map_add' _ _ := rfl
#align bilin_form.coe_fn_add_monoid_hom LinearMap.BilinForm.coeFnAddMonoidHom

instance {α} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] :
DistribMulAction α (BilinForm R M) := inferInstance

instance {α} [CommSemiring α] [Module α R] [SMulCommClass R α R] : Module α (BilinForm R M) :=
inferInstance

section flip

/-- Auxiliary construction for the flip of a bilinear form, obtained by exchanging the left and
Expand Down