mathlib3
chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map
#1062

Merged

chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map #1062

mergify merged 4 commits into master from to-linear-map-comp

jcommelin requested a review 6 years ago

chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map

ce9c8768

Stupid error

ad70f71d

ChrisHughes24 commented on 2019-05-20

Update src/ring_theory/algebra.lean

11e2888d

ChrisHughes24 dismissed these changes on 2019-05-20

mergify dismissed their stale review 6 years ago

Pull request has been modified.

ChrisHughes24 added ready-to-merge

ChrisHughes24 approved these changes on 2019-05-20

Merge branch 'master' into 'to-linear-map-comp'

665f6b7a

mergify merged 593938cd into master 6 years ago

mergify deleted the to-linear-map-comp branch 6 years ago

Reviewers

ChrisHughes24

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone