Skip to content

Commit 1fb0d6a

Browse files
FordUniverFordUniver
committed
merge: include feat/gradient-toDual (leanprover-community#39202) for Riesz isomorphism
2 parents 0c47526 + 7c7d969 commit 1fb0d6a

334 files changed

Lines changed: 7360 additions & 1459 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/shake.yaml‎

Lines changed: 143 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,143 @@
1+
name: shake
2+
3+
on:
4+
schedule:
5+
# Run several hours before the technical debt report which runs Mondays at 04:00 UTC
6+
- cron: "10 20 * * 0" # At 20:10 UTC on Sunday.
7+
workflow_dispatch:
8+
inputs:
9+
dry_run:
10+
description: 'If true, only scan and report without modifying files or opening a PR'
11+
required: false
12+
default: false
13+
type: boolean
14+
# auto_merge:
15+
# description: 'If true, apply the auto-merge-after-CI label when creating a PR'
16+
# required: false
17+
# default: true
18+
# type: boolean
19+
20+
jobs:
21+
build:
22+
name: lake shake --fix
23+
runs-on: ubuntu-latest
24+
if: github.repository == 'leanprover-community/mathlib4'
25+
permissions:
26+
contents: read
27+
id-token: write
28+
steps:
29+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
30+
31+
- name: Configure Lean
32+
uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
33+
with:
34+
auto-config: false
35+
use-github-cache: false
36+
use-mathlib-cache: true
37+
38+
- name: lake shake
39+
id: shake
40+
run: |
41+
lake shake --add-public --keep-implied --keep-prefix --fix --explain > explain.txt 2>&1
42+
if git diff --quiet; then
43+
echo "changed=false" >> "$GITHUB_OUTPUT"
44+
else
45+
echo "changed=true" >> "$GITHUB_OUTPUT"
46+
fi
47+
48+
- name: Parse shake stats
49+
id: stats
50+
if: steps.shake.outputs.changed == 'true'
51+
run: |
52+
scripts/parse_shake_output.py explain.txt "$GITHUB_OUTPUT"
53+
54+
- name: Upload explain.txt
55+
id: upload-artifact
56+
if: steps.shake.outputs.changed == 'true'
57+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
58+
with:
59+
name: shake-explain
60+
path: explain.txt
61+
62+
- name: Build PR body
63+
id: pr_body
64+
if: steps.shake.outputs.changed == 'true' && toJson(inputs.dry_run) != 'true'
65+
shell: bash
66+
env:
67+
RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
68+
ARTIFACT_ID: ${{ steps.upload-artifact.outputs.artifact-id }}
69+
CHANGED_FILES: ${{ steps.stats.outputs.changed_files }}
70+
ADDED: ${{ steps.stats.outputs.added }}
71+
REMOVED: ${{ steps.stats.outputs.removed }}
72+
run: |
73+
{
74+
echo "body<<EOF"
75+
echo "I am happy to shake some imports for you!"
76+
echo ""
77+
echo "**${CHANGED_FILES} files changed** · +${ADDED} imports added · -${REMOVED} imports removed"
78+
echo ""
79+
echo "---"
80+
echo ""
81+
echo "[workflow run for this PR](${RUN_URL})"
82+
echo "[explain.txt](${RUN_URL}/artifacts/${ARTIFACT_ID})"
83+
echo "EOF"
84+
} >> "$GITHUB_OUTPUT"
85+
86+
- name: Generate app token
87+
id: app-token
88+
if: steps.shake.outputs.changed == 'true' && toJson(inputs.dry_run) != 'true'
89+
uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760
90+
with:
91+
app-id: ${{ secrets.MATHLIB_NOLINTS_APP_ID }}
92+
key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }}
93+
key-name: mathlib-nolints-app-pk
94+
azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_PR_WRITERS }}
95+
azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }}
96+
97+
- name: Create Pull Request
98+
id: pr
99+
if: steps.shake.outputs.changed == 'true' && toJson(inputs.dry_run) != 'true'
100+
uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0
101+
with:
102+
author: "mathlib-nolints[bot] <258989889+mathlib-nolints[bot]@users.noreply.github.com>"
103+
token: "${{ steps.app-token.outputs.token }}"
104+
commit-message: |
105+
chore: lake shake --add-public --keep-implied --keep-prefix --fix
106+
107+
${{ steps.stats.outputs.changed_files }} files changed · +${{ steps.stats.outputs.added }} imports added · -${{ steps.stats.outputs.removed }} imports removed
108+
branch: "shake"
109+
base: master
110+
title: "chore: lake shake --add-public --keep-implied --keep-prefix --fix"
111+
body: ${{ steps.pr_body.outputs.body }}
112+
# labels: ${{ (github.event_name == 'schedule' || toJson(inputs.auto_merge) == 'true') && 'auto-merge-after-CI' || '' }}
113+
114+
- name: Send Zulip message (success)
115+
if: steps.pr.outcome == 'success'
116+
uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
117+
with:
118+
api-key: ${{ secrets.ZULIP_API_KEY }}
119+
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
120+
organization-url: 'https://leanprover.zulipchat.com'
121+
to: 'nightly-testing'
122+
type: 'stream'
123+
topic: 'Mathlib `shake --fix`'
124+
content: |
125+
Please review #${{ steps.pr.outputs.pull-request-number }} which changes
126+
${{ steps.stats.outputs.changed_files }} files:
127+
- +${{ steps.stats.outputs.added }} imports added
128+
- -${{ steps.stats.outputs.removed }} imports removed
129+
130+
- name: Send Zulip message (failure)
131+
if: ${{ toJson(inputs.dry_run) != 'true' && failure() }}
132+
uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
133+
with:
134+
api-key: ${{ secrets.ZULIP_API_KEY }}
135+
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
136+
organization-url: 'https://leanprover.zulipchat.com'
137+
to: 'nightly-testing'
138+
type: 'stream'
139+
topic: 'Mathlib `shake --fix`'
140+
content: |
141+
[`shake` workflow run failed](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})
142+
143+
triggered by: `${{ github.event_name }}`

‎Archive/Imo/Imo2025Q3.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -154,8 +154,8 @@ lemma isBonza : IsBonza fExample := by
154154
· simp [fExample, ch1]
155155
by_cases ch2 : a = 2
156156
· simp only [fExample, ch2, dvd_refl, not_true_eq_false, ↓reduceIte, Nat.cast_ofNat,
157-
Nat.two_dvd_ne_zero, Nat.cast_ite, Nat.cast_one, Nat.cast_pow, ite_pow, one_pow,
158-
Int.reducePow]
157+
Nat.two_dvd_ne_zero]
158+
push_cast
159159
split_ifs with hb1 hb2
160160
· grind [sq_mod_four_eq_one_of_odd]
161161
· simp [hb2]

‎Archive/Sensitivity.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -329,7 +329,7 @@ set_option backward.isDefEq.respectTransparency false in
329329
theorem g_injective : Injective (g m) := by
330330
rw [g]
331331
intro x₁ x₂ h
332-
simp only [V, LinearMap.prod_apply, LinearMap.id_apply, Prod.mk_inj, Pi.prod] at h
332+
simp only [V, LinearMap.prod_apply, LinearMap.id_apply, Prod.mk_inj, Function.prod_apply] at h
333333
exact h.right
334334

335335
set_option backward.isDefEq.respectTransparency false in

‎Mathlib.lean‎

Lines changed: 25 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -643,6 +643,7 @@ public import Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
643643
public import Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
644644
public import Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
645645
public import Mathlib.Algebra.Homology.HomotopyCofiber
646+
public import Mathlib.Algebra.Homology.HomotopyFiber
646647
public import Mathlib.Algebra.Homology.ImageToKernel
647648
public import Mathlib.Algebra.Homology.LeftResolution.Basic
648649
public import Mathlib.Algebra.Homology.LeftResolution.Reduced
@@ -1229,6 +1230,7 @@ public import Mathlib.Algebra.Ring.Idempotent
12291230
public import Mathlib.Algebra.Ring.Identities
12301231
public import Mathlib.Algebra.Ring.InjSurj
12311232
public import Mathlib.Algebra.Ring.Int.Defs
1233+
public import Mathlib.Algebra.Ring.Int.Field
12321234
public import Mathlib.Algebra.Ring.Int.Parity
12331235
public import Mathlib.Algebra.Ring.Int.Units
12341236
public import Mathlib.Algebra.Ring.Invertible
@@ -1378,11 +1380,13 @@ public import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
13781380
public import Mathlib.AlgebraicGeometry.Morphisms.Flat
13791381
public import Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
13801382
public import Mathlib.AlgebraicGeometry.Morphisms.FlatMono
1383+
public import Mathlib.AlgebraicGeometry.Morphisms.FlatRank
13811384
public import Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
13821385
public import Mathlib.AlgebraicGeometry.Morphisms.Immersion
13831386
public import Mathlib.AlgebraicGeometry.Morphisms.Integral
13841387
public import Mathlib.AlgebraicGeometry.Morphisms.IsIso
13851388
public import Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
1389+
public import Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent
13861390
public import Mathlib.AlgebraicGeometry.Morphisms.LocalIso
13871391
public import Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
13881392
public import Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
@@ -1488,8 +1492,10 @@ public import Mathlib.AlgebraicTopology.ModelCategory.Opposite
14881492
public import Mathlib.AlgebraicTopology.ModelCategory.Over
14891493
public import Mathlib.AlgebraicTopology.ModelCategory.PathObject
14901494
public import Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
1495+
public import Mathlib.AlgebraicTopology.ModelCategory.Transport
14911496
public import Mathlib.AlgebraicTopology.MooreComplex
14921497
public import Mathlib.AlgebraicTopology.Quasicategory.Basic
1498+
public import Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
14931499
public import Mathlib.AlgebraicTopology.Quasicategory.Nerve
14941500
public import Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory
14951501
public import Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
@@ -1516,11 +1522,13 @@ public import Mathlib.AlgebraicTopology.SimplicialNerve
15161522
public import Mathlib.AlgebraicTopology.SimplicialObject.Basic
15171523
public import Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
15181524
public import Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
1525+
public import Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
15191526
public import Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
15201527
public import Mathlib.AlgebraicTopology.SimplicialObject.II
15211528
public import Mathlib.AlgebraicTopology.SimplicialObject.Op
15221529
public import Mathlib.AlgebraicTopology.SimplicialObject.Split
15231530
public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
1531+
public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
15241532
public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
15251533
public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
15261534
public import Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
@@ -1863,6 +1871,7 @@ public import Mathlib.Analysis.Complex.UpperHalfPlane.Metric
18631871
public import Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
18641872
public import Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
18651873
public import Mathlib.Analysis.Complex.UpperHalfPlane.Topology
1874+
public import Mathlib.Analysis.Complex.ValueDistribution.Cartan
18661875
public import Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
18671876
public import Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
18681877
public import Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
@@ -2719,6 +2728,7 @@ public import Mathlib.CategoryTheory.Groupoid.Grpd.Basic
27192728
public import Mathlib.CategoryTheory.Groupoid.Subgroupoid
27202729
public import Mathlib.CategoryTheory.Groupoid.VertexGroup
27212730
public import Mathlib.CategoryTheory.GuitartExact.Basic
2731+
public import Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
27222732
public import Mathlib.CategoryTheory.GuitartExact.KanExtension
27232733
public import Mathlib.CategoryTheory.GuitartExact.Opposite
27242734
public import Mathlib.CategoryTheory.GuitartExact.Over
@@ -2966,6 +2976,7 @@ public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
29662976
public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
29672977
public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
29682978
public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
2979+
public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
29692980
public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
29702981
public import Mathlib.CategoryTheory.Localization.Equivalence
29712982
public import Mathlib.CategoryTheory.Localization.FiniteProducts
@@ -3038,6 +3049,7 @@ public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
30383049
public import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_
30393050
public import Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
30403051
public import Mathlib.CategoryTheory.Monoidal.Cartesian.Over
3052+
public import Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
30413053
public import Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
30423054
public import Mathlib.CategoryTheory.Monoidal.Category
30433055
public import Mathlib.CategoryTheory.Monoidal.Center
@@ -3417,6 +3429,7 @@ public import Mathlib.CategoryTheory.Triangulated.Basic
34173429
public import Mathlib.CategoryTheory.Triangulated.Functor
34183430
public import Mathlib.CategoryTheory.Triangulated.Generators
34193431
public import Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
3432+
public import Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
34203433
public import Mathlib.CategoryTheory.Triangulated.Opposite.Basic
34213434
public import Mathlib.CategoryTheory.Triangulated.Opposite.Functor
34223435
public import Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
@@ -4487,6 +4500,8 @@ public import Mathlib.Geometry.Convex.Cone.DualFinite
44874500
public import Mathlib.Geometry.Convex.Cone.Pointed
44884501
public import Mathlib.Geometry.Convex.Cone.Simplicial
44894502
public import Mathlib.Geometry.Convex.Cone.TensorProduct
4503+
public import Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
4504+
public import Mathlib.Geometry.Convex.ConvexSpace.Defs
44904505
public import Mathlib.Geometry.Diffeology.Basic
44914506
public import Mathlib.Geometry.Euclidean.Altitude
44924507
public import Mathlib.Geometry.Euclidean.Angle.Bisector
@@ -4531,6 +4546,7 @@ public import Mathlib.Geometry.Group.Growth.QuotientInter
45314546
public import Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
45324547
public import Mathlib.Geometry.Manifold.Algebra.LieGroup
45334548
public import Mathlib.Geometry.Manifold.Algebra.Monoid
4549+
public import Mathlib.Geometry.Manifold.Algebra.SMul
45344550
public import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
45354551
public import Mathlib.Geometry.Manifold.Algebra.Structures
45364552
public import Mathlib.Geometry.Manifold.Bordism
@@ -4886,8 +4902,6 @@ public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
48864902
public import Mathlib.LinearAlgebra.Complex.Module
48874903
public import Mathlib.LinearAlgebra.Complex.Orientation
48884904
public import Mathlib.LinearAlgebra.Contraction
4889-
public import Mathlib.LinearAlgebra.ConvexSpace
4890-
public import Mathlib.LinearAlgebra.ConvexSpace.AffineSpace
48914905
public import Mathlib.LinearAlgebra.Countable
48924906
public import Mathlib.LinearAlgebra.CrossProduct
48934907
public import Mathlib.LinearAlgebra.DFinsupp
@@ -5672,7 +5686,6 @@ public import Mathlib.NumberTheory.ModularForms.Cusps
56725686
public import Mathlib.NumberTheory.ModularForms.DedekindEta
56735687
public import Mathlib.NumberTheory.ModularForms.Delta
56745688
public import Mathlib.NumberTheory.ModularForms.Derivative
5675-
public import Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne
56765689
public import Mathlib.NumberTheory.ModularForms.Discriminant
56775690
public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
56785691
public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
@@ -5690,7 +5703,9 @@ public import Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
56905703
public import Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold
56915704
public import Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
56925705
public import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
5693-
public import Mathlib.NumberTheory.ModularForms.LevelOne
5706+
public import Mathlib.NumberTheory.ModularForms.LevelOne.Basic
5707+
public import Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
5708+
public import Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
56945709
public import Mathlib.NumberTheory.ModularForms.NormTrace
56955710
public import Mathlib.NumberTheory.ModularForms.Petersson
56965711
public import Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
@@ -5726,6 +5741,7 @@ public import Mathlib.NumberTheory.NumberField.Discriminant.Basic
57265741
public import Mathlib.NumberTheory.NumberField.Discriminant.Defs
57275742
public import Mathlib.NumberTheory.NumberField.Discriminant.Different
57285743
public import Mathlib.NumberTheory.NumberField.EquivReindex
5744+
public import Mathlib.NumberTheory.NumberField.ExistsRamified
57295745
public import Mathlib.NumberTheory.NumberField.FinitePlaces
57305746
public import Mathlib.NumberTheory.NumberField.FractionalIdeal
57315747
public import Mathlib.NumberTheory.NumberField.House
@@ -6488,6 +6504,7 @@ public import Mathlib.RingTheory.Ideal.GoingUp
64886504
public import Mathlib.RingTheory.Ideal.Height
64896505
public import Mathlib.RingTheory.Ideal.IdempotentFG
64906506
public import Mathlib.RingTheory.Ideal.Int
6507+
public import Mathlib.RingTheory.Ideal.IsAugmentation
64916508
public import Mathlib.RingTheory.Ideal.IsPrimary
64926509
public import Mathlib.RingTheory.Ideal.IsPrincipal
64936510
public import Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
@@ -6566,6 +6583,7 @@ public import Mathlib.RingTheory.LaurentSeries
65666583
public import Mathlib.RingTheory.Length
65676584
public import Mathlib.RingTheory.LinearDisjoint
65686585
public import Mathlib.RingTheory.LittleWedderburn
6586+
public import Mathlib.RingTheory.LocalIso
65696587
public import Mathlib.RingTheory.LocalProperties.Basic
65706588
public import Mathlib.RingTheory.LocalProperties.Exactness
65716589
public import Mathlib.RingTheory.LocalProperties.Injective
@@ -6955,7 +6973,8 @@ public import Mathlib.RingTheory.ZariskisMainTheorem
69556973
public import Mathlib.SetTheory.Cardinal.Aleph
69566974
public import Mathlib.SetTheory.Cardinal.Arithmetic
69576975
public import Mathlib.SetTheory.Cardinal.Basic
6958-
public import Mathlib.SetTheory.Cardinal.Cofinality
6976+
public import Mathlib.SetTheory.Cardinal.Cofinality.Basic
6977+
public import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
69596978
public import Mathlib.SetTheory.Cardinal.Continuum
69606979
public import Mathlib.SetTheory.Cardinal.CountableCover
69616980
public import Mathlib.SetTheory.Cardinal.Defs
@@ -7719,6 +7738,7 @@ public import Mathlib.Topology.Instances.AddCircle.Real
77197738
public import Mathlib.Topology.Instances.CantorSet
77207739
public import Mathlib.Topology.Instances.Complex
77217740
public import Mathlib.Topology.Instances.Discrete
7741+
public import Mathlib.Topology.Instances.ENNReal.ENatENNReal
77227742
public import Mathlib.Topology.Instances.ENNReal.Lemmas
77237743
public import Mathlib.Topology.Instances.ENat
77247744
public import Mathlib.Topology.Instances.EReal.Lemmas

‎Mathlib/Algebra/Algebra/NonUnitalHom.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -371,13 +371,13 @@ variable [DistribMulAction R C]
371371
/-- The prod of two morphisms is a morphism. -/
372372
@[simps]
373373
def prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : A →ₙₐ[R] B × C where
374-
toFun := Pi.prod f g
375-
map_zero' := by simp only [Pi.prod, Prod.mk_zero_zero, map_zero]
376-
map_add' x y := by simp only [Pi.prod, Prod.mk_add_mk, map_add]
377-
map_mul' x y := by simp only [Pi.prod, Prod.mk_mul_mk, map_mul]
378-
map_smul' c x := by simp only [Pi.prod, map_smul, MonoidHom.id_apply, Prod.smul_mk]
374+
toFun := Function.prod f g
375+
map_zero' := by simp only [Function.prod_apply, Prod.mk_zero_zero, map_zero]
376+
map_add' x y := by simp only [Function.prod_apply, Prod.mk_add_mk, map_add]
377+
map_mul' x y := by simp only [Function.prod_apply, Prod.mk_mul_mk, map_mul]
378+
map_smul' c x := by simp only [Function.prod_apply, map_smul, MonoidHom.id_apply, Prod.smul_mk]
379379

380-
theorem coe_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : ⇑(f.prod g) = Pi.prod f g :=
380+
theorem coe_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : ⇑(f.prod g) = Function.prod f g :=
381381
rfl
382382

383383
@[simp]
@@ -390,7 +390,7 @@ theorem snd_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : (snd R B C).com
390390

391391
@[simp]
392392
theorem prod_fst_snd : prod (fst R A B) (snd R A B) = 1 :=
393-
coe_injective Pi.prod_fst_snd
393+
coe_injective Function.prod_fst_snd
394394

395395
/-- Taking the product of two maps with the same domain is equivalent to taking the product of
396396
their codomains. -/

0 commit comments

Comments
 (0)