Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit f00ab96

Browse files
fix(analysis/normed_space/bounded_linear_maps): fix build
1 parent 31ff5c5 commit f00ab96

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/analysis/normed_space/bounded_linear_maps.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,7 @@ end
118118

119119
end is_bounded_linear_map
120120

121-
set_option class.instance_max_depth 35
121+
set_option class.instance_max_depth 60
122122

123123
/-- A continuous linear map between normed spaces is bounded when the field is nondiscrete.
124124
The continuity ensures boundedness on a ball of some radius δ. The nondiscreteness is then

0 commit comments

Comments
 (0)