Skip to content
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

Jump to bottom

[Merged by Bors] - fix: shorter names for some instances #6123

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - fix: shorter names for some instances #6123

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
3d6b22d
fix: shorter names for some instances
kbuzzard Jul 25, 2023
9bc8219
add a third long name
kbuzzard Jul 25, 2023
a124fe0
tidy up
kbuzzard Jul 25, 2023
bf75387
more with-removal
kbuzzard Jul 25, 2023
408419a
new instance name is shorter, at least...
kbuzzard Jul 25, 2023
4fef7ea
fix another instance name
kbuzzard Jul 25, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
10 changes: 5 additions & 5 deletions Mathlib/RingTheory/TensorProduct.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -436,7 +436,7 @@ instance : AddMonoidWithOne (A ⊗[R] B) :=

instance : AddCommMonoid (A ⊗[R] B) := by infer_instance

instance : Semiring (A ⊗[R] B) :=
instance instSemiring : Semiring (A ⊗[R] B) :=
{ (by infer_instance : AddMonoidWithOne (A ⊗[R] B)),
(by infer_instance : AddCommMonoid (A ⊗[R] B)) with
zero := 0
Expand Down Expand Up @@ -582,8 +582,8 @@ variable {A : Type v₁} [Ring A] [Algebra R A]

variable {B : Type v₂} [Ring B] [Algebra R B]

instance : Ring (A ⊗[R] B) :=
{ (by infer_instance : Semiring (A ⊗[R] B)) with
instance instRing : Ring (A ⊗[R] B) :=
{ toSemiring := inferInstance
add_left_neg := add_left_neg }

end Ring
Expand All @@ -596,8 +596,8 @@ variable {A : Type v₁} [CommRing A] [Algebra R A]

variable {B : Type v₂} [CommRing B] [Algebra R B]

instance : CommRing (A ⊗[R] B) :=
{ (by infer_instance : Ring (A ⊗[R] B)) with
instance instCommRing : CommRing (A ⊗[R] B) :=
{ toRing := inferInstance
mul_comm := fun x y => by
refine TensorProduct.induction_on x ?_ ?_ ?_
· simp
Expand Down
2 changes: 1 addition & 1 deletion docs/overview.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ General algebra:
associative algebra over a commutative ring: 'Algebra'
the category of algebras over a ring: 'AlgebraCat'
free algebra of a commutative ring: 'FreeAlgebra'
tensor product of algebras: 'Algebra.TensorProduct.instAlgebraTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModuleInstSemiringTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModule'
tensor product of algebras: 'Algebra.TensorProduct.instAlgebraTensorProductToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleToModuleInstSemiring'
kbuzzard marked this conversation as resolved.
Show resolved Hide resolved
tensor algebra of a commutative ring: 'TensorAlgebra'
Lie algebra: 'LieAlgebra'
exterior algebra: 'ExteriorAlgebra'
Expand Down