[Merged by Bors] - fix(algebra/module/basic): Do not attach the ℕ and ℤ is_scalar_tower and smul_comm_class instances to a specific definition of smul
#5509
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…` and `smul_comm_class` instances to a specific definition of smul These instances are in `Prop`, so the more the merrier. Without this change, these instances are not available for alternative ℤ-module definitions.
eric-wieser
added
the
awaiting-review
|
let's merge this one, everyone seemed to agree on Zulip |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jan 3, 2021
…` and `smul_comm_class` instances to a specific definition of smul (#5509) These instances are in `Prop`, so the more the merrier. Without this change, these instances are not available for alternative ℤ-module definitions. An example of one of these alternate definitions is `linear_map.semimodule`, which provide a second non-defeq ℤ-module structure alongside `add_comm_group.int_module`. With this PR, both semimodule structures are shown to satisfy `smul_comm_class` and `is_scalar_tower`; while before it, only `add_comm_group.int_module` was shown to satisfy these. This PR makes the following work: ```lean example {R : Type*} {M₁ M₂ M₃ : Type*} [comm_semiring R] [add_comm_monoid M₁] [semimodule R M₁] [add_comm_monoid M₂] [semimodule R M₂] [add_comm_monoid M₃] [semimodule R M₃] (f : M₁ →ₗ[R] M₂ →ₗ[R] M₃) (x : M₁) (n : ℕ) : f (n • x) = n • f x := by simp ```
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
is_scalar_tower and smul_comm_class instances to a specific definition of smulis_scalar_tower and smul_comm_class instances to a specific definition of smul
pglutz
pushed a commit
that referenced
this pull request
Jan 6, 2021
…` and `smul_comm_class` instances to a specific definition of smul (#5509) These instances are in `Prop`, so the more the merrier. Without this change, these instances are not available for alternative ℤ-module definitions. An example of one of these alternate definitions is `linear_map.semimodule`, which provide a second non-defeq ℤ-module structure alongside `add_comm_group.int_module`. With this PR, both semimodule structures are shown to satisfy `smul_comm_class` and `is_scalar_tower`; while before it, only `add_comm_group.int_module` was shown to satisfy these. This PR makes the following work: ```lean example {R : Type*} {M₁ M₂ M₃ : Type*} [comm_semiring R] [add_comm_monoid M₁] [semimodule R M₁] [add_comm_monoid M₂] [semimodule R M₂] [add_comm_monoid M₃] [semimodule R M₃] (f : M₁ →ₗ[R] M₂ →ₗ[R] M₃) (x : M₁) (n : ℕ) : f (n • x) = n • f x := by simp ```
eric-wieser
changed the title
is_scalar_tower and smul_comm_class instances to a specific definition of smulℕ and ℤ is_scalar_tower and smul_comm_class instances to a specific definition of smul
eric-wieser
changed the title
ℕ and ℤ is_scalar_tower and smul_comm_class instances to a specific definition of smulℕ and ℤ is_scalar_tower and smul_comm_class instances to a specific definition of smul
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
These instances are in
Prop, so the more the merrier.Without this change, these instances are not available for alternative ℤ-module definitions.
An example of one of these alternate definitions is
linear_map.semimodule, which provide a second non-defeq ℤ-module structure alongsideadd_comm_group.int_module.With this PR, both semimodule structures are shown to satisfy
smul_comm_classandis_scalar_tower; while before it, onlyadd_comm_group.int_modulewas shown to satisfy these.This PR makes the following work:
Zulip