Skip to content

Commit f4bf901

Browse files
goliath-kleingoliath-klein
committed
actually weaken to
1 parent ed2acc8 commit f4bf901

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

‎Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ namespace PiTensorProduct
5151

5252
section NormedField
5353

54-
variable [NontriviallyNormedField 𝕜]
54+
variable [NormedField 𝕜]
5555

5656
/-- A lift of the projective seminorm to `FreeAddMonoid (𝕜 × Π i, Eᵢ)`, useful to prove the
5757
properties of `projectiveSeminorm`. -/

0 commit comments

Comments
 (0)